not_le_iff_exists — Mathlib

English

A subspace is not contained in another if and only if there exists a point in the first that is not in the second.

Русский

Подпространство не содержится в другое тогда и только тогда, когда существует точка p ∈ s1, такая что p ∉ s2.

LaTeX

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

Lean4

/-- One subspace is not less than or equal to another if and only if it has a point not in the
second subspace. -/
theorem not_le_iff_exists (s₁ s₂ : AffineSubspace k P) : ¬s₁ ≤ s₂ ↔ ∃ p ∈ s₁, p ∉ s₂ :=
  Set.not_subset

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