inter_nonempty_of_nonempty_of_sup_direction_eq_top

English

If the directions of two nonempty affine subspaces span the whole space, their intersection is nonempty.

Русский

Если направления двух непустых аффинных подпроизвольных порождают всё пространство, их пересечение непусто.

LaTeX

$$$\text{If } s_1, s_2 \text{ are nonempty and } s_1.direction \sqcup s_2.direction = \top, \text{ then } (s_1 \cap s_2) \neq \emptyset.$$$

Lean4

/-- If the directions of two nonempty affine subspaces span the whole module, they have nonempty
intersection. -/
theorem inter_nonempty_of_nonempty_of_sup_direction_eq_top {s₁ s₂ : AffineSubspace k P} (h1 : (s₁ : Set P).Nonempty)
    (h2 : (s₂ : Set P).Nonempty) (hd : s₁.direction ⊔ s₂.direction = ⊤) : ((s₁ : Set P) ∩ s₂).Nonempty :=
  by
  by_contra h
  rw [Set.not_nonempty_iff_eq_empty] at h
  have hlt := sup_direction_lt_of_nonempty_of_inter_empty h1 h2 h
  rw [hd] at hlt
  exact not_top_lt hlt

Похожие утверждения