lt_iff_le_and_exists — Mathlib

English

A subspace is strictly contained in another iff it is contained and there exists a point in the second not in the first.

Русский

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

LaTeX

$$$s_1 < s_2 \\iff (s_1 \\le s_2) \\land \\exists p \\in s_2, p \\notin s_1$$$

Lean4

/-- A subspace is less than another if and only if it is less than or equal to the second subspace
and there is a point only in the second. -/
theorem lt_iff_le_and_exists (s₁ s₂ : AffineSubspace k P) : s₁ < s₂ ↔ s₁ ≤ s₂ ∧ ∃ p ∈ s₂, p ∉ s₁ := by
  rw [lt_iff_le_not_ge, not_le_iff_exists]

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