English
If the directions are complementary, two nonempty affine subspaces intersect in exactly one point.
Русский
Если направления комплементарны, две непустые аффинные подпространства пересекаются в ровно одной точке.
LaTeX
$$$\text{If } s_1, s_2 \text{ are nonempty and } IsCompl(s_1.direction, s_2.direction), \ \ (s_1 \cap s_2) = \{p\} \text{ for some } p.$$$
Lean4
/-- If the directions of two nonempty affine subspaces are complements of each other, they intersect
in exactly one point. -/
theorem inter_eq_singleton_of_nonempty_of_isCompl {s₁ s₂ : AffineSubspace k P} (h1 : (s₁ : Set P).Nonempty)
(h2 : (s₂ : Set P).Nonempty) (hd : IsCompl s₁.direction s₂.direction) : ∃ p, (s₁ : Set P) ∩ s₂ = { p } :=
by
obtain ⟨p, hp⟩ := inter_nonempty_of_nonempty_of_sup_direction_eq_top h1 h2 hd.sup_eq_top
use p
ext q
rw [Set.mem_singleton_iff]
constructor
· rintro ⟨hq1, hq2⟩
have hqp : q -ᵥ p ∈ s₁.direction ⊓ s₂.direction := ⟨vsub_mem_direction hq1 hp.1, vsub_mem_direction hq2 hp.2⟩
rwa [hd.inf_eq_bot, Submodule.mem_bot, vsub_eq_zero_iff_eq] at hqp
· exact fun h => h.symm ▸ hp
