ssubset_singleton_iff — Mathlib

English

A nontrivial proper subset of a singleton is impossible; s ⊂ {x} iff s = ∅.

Русский

Непустое строгие подмножество единичного множества невозможно; s ⊂ {x} тогда и только тогда, что s = ∅.

LaTeX

$$$s \subsetneq \{x\} \iff s = \emptyset$$$

Lean4

theorem ssubset_singleton_iff {s : Set α} {x : α} : s ⊂ { x } ↔ s = ∅ :=
  by
  rw [ssubset_iff_subset_ne, subset_singleton_iff_eq, or_and_right, and_not_self_iff, or_false, and_iff_left_iff_imp]
  exact fun h => h ▸ (singleton_ne_empty _).symm

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