def AffineBuilding.Sector.Parallel {V : Type} [DecidableEq V] (b : Building V) (S₁ S₂ : Sector b) : Prop

Two sectors are parallel if they share a common subsector $T$ with $T \subseteq S_1$ and $T \subseteq S_2$ (Section 16.6).

theorem AffineBuilding.Sector.Parallel.to_sameDirection {V : Type} [DecidableEq V] {b : Building V} {S₁ S₂ : Sector b} (h : Parallel b S₁ S₂) : SameDirection b S₁ S₂

Sector parallelism implies pointing in the same direction.

theorem AffineBuilding.Sector.SameDirection.to_parallel {V : Type} [DecidableEq V] {b : Building V} {S₁ S₂ : Sector b} (h : SameDirection b S₁ S₂) : Parallel b S₁ S₂

Conversely, sectors with the same direction are parallel — the two notions agree.

theorem AffineBuilding.same_direction_same_half_apartment_side {V : Type} [DecidableEq V] (b : Building V) (S : Sector b) (eta : Wall b) (H : HalfApartment b) (heta_apt : eta.apartment = S.apartment) (hwall : H.wall = eta) (T₁ : Sector b) (hT₁_sub : Sector.Subsector b T₁ S) (hT₁_in_H : ∀ v ∈ T₁.vertices, v ∈ H.vertices) (T₂ : Sector b) (hT₂_sub : Sector.Subsector b T₂ S) : ∃ (U : Sector b), Sector.Subsector b U T₂ ∧ ∀ v ∈ U.vertices, v ∈ H.vertices

If $T_1 \subseteq S$ lies in a half-apartment $H$ bounded by wall $\eta$, then every subsector $T_2 \subseteq S$ has a further subsector $U$ also lying in $H$ — parallel sectors agree on which side of $\eta$ they sit.

theorem AffineBuilding.parallel_sectors_same_positive_half_apartment {V : Type} [DecidableEq V] {b : Building V} {S₁ S₂ : Sector b} {eta : Wall b} {H : HalfApartment b} (hpar : Sector.SameDirection b S₁ S₂) (heta_apt₁ : eta.apartment = S₁.apartment) (heta_apt₂ : eta.apartment = S₂.apartment) (hpos : IsPositiveHalfApartment S₁ eta H) : IsPositiveHalfApartment S₂ eta H

Parallel sectors $S_1, S_2$ share the same positive half-apartment with respect to a wall $\eta$: if $H$ is positive for $S_1$, it is positive for $S_2$.