subset_insert_iff — Mathlib

English

For any s,t and a, s ⊆ insert a t is equivalent to (s ⊆ t) or (a ∈ s and s \ {a} ⊆ t).

Русский

Для множества s, t и элемента a верно: s ⊆ insert a t тогда и только тогда, когда s ⊆ t или (a ∈ s и s \ {a} ⊆ t).

LaTeX

$$$$ s \subseteq \text{insert } a t \iff \bigl(s \subseteq t \bigr) \lor \bigl(a \in s \wedge (s \setminus \{a\}) \subseteq t\bigr). $$$$

Lean4

theorem subset_insert_iff : s ⊆ insert a t ↔ s ⊆ t ∨ (a ∈ s ∧ s \ { a } ⊆ t) := by grind

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