ssubset_iff_exists — Mathlib

English

Let S and T be sets. A strict subset S ⊊ T holds if and only if S ⊆ T and there exists x ∈ T with x ∉ S.

Русский

Пусть S, T — множества. Тогда S ⊊ T эквивалентно тому, что S ⊆ T и существует x ∈ T, такой что x ∉ S.

LaTeX

$$$ s \subsetneq t \iff (s \subseteq t \wedge \exists x \in t, x \notin s) $$$

Lean4

theorem ssubset_iff_exists {s t : Set α} : s ⊂ t ↔ s ⊆ t ∧ ∃ x ∈ t, x ∉ s :=
  ⟨fun h ↦ ⟨h.le, Set.exists_of_ssubset h⟩, fun ⟨h1, h2⟩ ↦ (Set.ssubset_iff_of_subset h1).mpr h2⟩

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