direction_inf_of_mem — Mathlib

English

If two affine subspaces share a point, the direction of their infimum equals the infimum of their directions.

Русский

Если две аффинные подпосотности имеют общую точку, направление их пересечения равно пересечению направлений.

LaTeX

$$$\text{If } p \in s_1 \cap s_2:\; (s_1 \sqcap s_2).direction = s_1.direction \cap s_2.direction$$$

Lean4

/-- If two affine subspaces have a point in common, the direction of their inf equals the inf of
their directions. -/
theorem direction_inf_of_mem {s₁ s₂ : AffineSubspace k P} {p : P} (h₁ : p ∈ s₁) (h₂ : p ∈ s₂) :
    (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction := by
  ext v
  rw [Submodule.mem_inf, ← vadd_mem_iff_mem_direction v h₁, ← vadd_mem_iff_mem_direction v h₂, ←
    vadd_mem_iff_mem_direction v ((mem_inf_iff p s₁ s₂).2 ⟨h₁, h₂⟩), mem_inf_iff]

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