toFinset_union — Mathlib

English

If (s ∪ t) is finite, then its Finset equals the union of the Finsets: h.toFinset = hs.toFinset ∪ ht.toFinset.

Русский

Если (s ∪ t) конечно, то соответствующий Finset равен объединению Finset: h.toFinset = hs.toFinset ∪ ht.toFinset.

LaTeX

$$$ h.toFinset = hs.toFinset \cup ht.toFinset $$$

Lean4

protected theorem toFinset_union [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s ∪ t).Finite) :
    h.toFinset = hs.toFinset ∪ ht.toFinset := by
  ext
  simp

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