cons_subset — Mathlib

English

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

Русский

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

LaTeX

$$$\forall s,t: Finset\,\alpha\,\forall a: \alpha\,\forall h: a \notin s:\ (s \cup \{a\}) \subseteq t \iff a \in t \wedge s \subseteq t$$$

Lean4

theorem cons_subset {h : a ∉ s} : s.cons a h ⊆ t ↔ a ∈ t ∧ s ⊆ t :=
  Multiset.cons_subset

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