singleton_disjUnion — Mathlib

English

For a and t with Disjoint {a} and t, disjUnion {a} t h equals cons a t with h-projection.

Русский

Для {a} и t при Disjoint {a} t, disjUnion {a} t совпадает с добавлением a в голову t.

LaTeX

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

Lean4

theorem singleton_disjUnion (a : α) (t : Finset α) (h : Disjoint { a } t) :
    disjUnion { a } t h = cons a t (disjoint_singleton_left.mp h) :=
  eq_of_veq <| Multiset.singleton_add _ _

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