le_def' — Mathlib

English

Let s1 and s2 be affine subspaces. Then s1 is contained in s2 if and only if every point of s1 lies in s2.

Русский

Пусть s1 и s2 — аффинные подпространства. Тогда s1 ⊆ s2 тогда и только тогда, когда любая точка p из s1 принадлежит s2.

LaTeX

$$$s_1 \\le s_2 \\iff \\forall p \\in s_1,\\ p \\in s_2$$$

Lean4

/-- One subspace is less than or equal to another if and only if all its points are in the second
subspace. -/
theorem le_def' (s₁ s₂ : AffineSubspace k P) : s₁ ≤ s₂ ↔ ∀ p ∈ s₁, p ∈ s₂ :=
  Iff.rfl

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