cons_subset_cons — Mathlib

English

Let s,t be finite sets and a ∉ s, a ∉ t. Then s ∪ {a} ⊆ t ∪ {a} if and only if s ⊆ t.

Русский

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

LaTeX

$$$\forall s,t: Finset\,\alpha\,\forall a: α\,\forall hs: a \notin s\,\forall ht: a \notin t:\ (s \cup \{a\}) \subseteq (t \cup \{a\}) \iff s \subseteq t$$$

Lean4

@[simp]
theorem cons_subset_cons {hs ht} : s.cons a hs ⊆ t.cons a ht ↔ s ⊆ t := by
  rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]

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