direction_inf_of_mem_inf — Mathlib

English

A point lies in the infimum of a set of affine subspaces iff it lies in every member of the set.

Русский

Точка лежит в infimum множества аффинных подплощадей тогда и только тогда, когда она лежит в каждой из них.

LaTeX

$$$p \in sInf t \iff \forall s \in t, p \in s$$$

Lean4

/-- If two affine subspaces have a point in their inf, the direction of their inf equals the inf of
their directions. -/
theorem direction_inf_of_mem_inf {s₁ s₂ : AffineSubspace k P} {p : P} (h : p ∈ s₁ ⊓ s₂) :
    (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction :=
  direction_inf_of_mem ((mem_inf_iff p s₁ s₂).1 h).1 ((mem_inf_iff p s₁ s₂).1 h).2

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