theorem GeometricAlgebra.opposite_flags_same_len {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F'₁ F'₂ : Flag k V) (h₁ : F.isOppositeFlag F'₁) (h₂ : F.isOppositeFlag F'₂) : F'₁.len = F'₂.len

Two flags opposite to the same flag F necessarily share the same length.

theorem GeometricAlgebra.isOppositeFlag_sup_eq_top {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F' : Flag k V) (h : F.isOppositeFlag F') (i : Fin F.len) : have j := ⟨F'.len - 1 - ↑i, ⋯⟩; F.spaces i ⊔ F'.spaces j = ⊤

Codisjointness of opposite flags: each level F.spaces i together with the matching level F'.spaces (F'.len - 1 - i) of the opposite flag spans V.

theorem GeometricAlgebra.isOppositeFlag_inf_eq_bot {k : Type u_1} [Field k] {V : Type u_2} [AddCommGroup V] [Module k V] (F F' : Flag k V) (h : F.isOppositeFlag F') (i : Fin F.len) : have j := ⟨F'.len - 1 - ↑i, ⋯⟩; F.spaces i ⊓ F'.spaces j = ⊥

Disjointness of opposite flags: each level F.spaces i and the matching level F'.spaces (F'.len - 1 - i) of the opposite flag intersect trivially.