insert_subset_insert — Mathlib

English

To prove a property for all Finset α, it suffices to prove it for the empty Finset and to show that if it holds for s, then it holds for insert a s with a ∉ s.

Русский

Чтобы доказать свойство для всех Finset α, достаточно доказать его для пустого Finset и показать, что если оно верно для s, то верно и для insert a s при a ∉ s.

LaTeX

$$$\\text{If } P(\\emptyset) \\text{ and } \\forall a\\, s\\ (ha:\\ a \\notin s), P(s) \\Rightarrow P(\\operatorname{insert}(a,s)) \\text{ then } \\forall s\\ P(s)$$$

Lean4

@[gcongr, simp]
theorem insert_subset_insert (a : α) {s t : Finset α} (h : s ⊆ t) : insert a s ⊆ insert a t := by grind

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