subset_insert_iff — Mathlib

English

Let α be a type with decidable equality and s, t be finite subsets of α, and a an element of α. Then s is contained in insert a t if and only if s with a removed is contained in t.

Русский

Пусть α — множество с разрешимой эквивалентностью, s и t — конечные подмножества α, а a — элемент α. Тогда s ⊆ insert a t тогда и только тогда, когда s \ {a} ⊆ t.

LaTeX

$$$ \\forall \\alpha [DecidableEq \\alpha], \\forall a : \\alpha, \\forall s,t : Finset \\alpha,\\\\ s \\subseteq insert\\ a\\ t \\iff erase\\ s\\ a \\subseteq t$$$

Lean4

theorem subset_insert_iff {a : α} {s t : Finset α} : s ⊆ insert a t ↔ erase s a ⊆ t := by grind

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