coe_disjUnion — Mathlib

English

The coe version of disjUnion preserves disjointness relations: (disjUnion s t h).toSet = s.toSet ∪ t.toSet.

Русский

Версия через образ сохраняет отношение непересечения: (disjUnion s t h).toSet = s.toSet ∪ t.toSet.

LaTeX

$$$\\operatorname{toSet}(\\operatorname{disjUnion}(s,t,h)) = \\operatorname{toSet}(s) \\cup \\operatorname{toSet}(t)$$$

Lean4

@[simp, norm_cast]
theorem coe_disjUnion {s t : Finset α} (h : Disjoint s t) : (disjUnion s t h : Set α) = (s : Set α) ∪ t :=
  Set.ext <| by simp

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