disjUnion_singleton — Mathlib

English

DisjUnion s (singleton a) h equals cons a s with h-projection.

Русский

DisjUnion s {a} h равняется добавлению a перед s.

LaTeX

$$$\\operatorname{disjUnion}(s, \\{a\\}, h) = \\operatorname{cons}(a, s, \\text{disjoint_singleton_right.mp}(h))$$$

Lean4

theorem disjUnion_singleton (s : Finset α) (a : α) (h : Disjoint s { a }) :
    disjUnion s { a } h = cons a s (disjoint_singleton_right.mp h) := by rw [disjUnion_comm, singleton_disjUnion]

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