exists_of_lt — Mathlib

English

If a subspace is strictly contained in another, there exists a point in the second that is not in the first.

Русский

Если подпространство строго вложено в другое, существует точка во втором, которая не принадлежит первому.

LaTeX

$$$s_1 < s_2 \\Rightarrow \\exists p \\in s_2, p \\notin s_1$$$

Lean4

/-- If a subspace is less than another, there is a point only in the second. -/
theorem exists_of_lt {s₁ s₂ : AffineSubspace k P} (h : s₁ < s₂) : ∃ p ∈ s₂, p ∉ s₁ :=
  Set.exists_of_ssubset h

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