ssubset_iff_exists_cons_subset — Mathlib

English

Let s,t be finite sets. Then s is a proper subset of t if and only if there exists an element a not in s such that s ∪ {a} ⊆ t.

Русский

Пусть s,t — конечные множества. Тогда s ⊂ t тогда и только если существует элемент a, не принадлежащий s, такой что s ∪ {a} ⊆ t.

LaTeX

$$$\forall s,t: Finset\,\alpha:\ s \subset t \iff \exists a: α, a \notin s ∧ s \cup \{a\} \subseteq t$$$

Lean4

theorem ssubset_iff_exists_cons_subset : s ⊂ t ↔ ∃ (a : _) (h : a ∉ s), s.cons a h ⊆ t := by grind

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