coe_sups — Mathlib

English

A simp-lemma equates the Set-side sups with the Finset-side sups under toSet and hasSups.

Русский

Лемма-упрощение увязывает множества-стороны супов с множествами Finset через toSet и hasSups.

LaTeX

$$$ \\operatorname{Set.hasSups.sups}(s^{\\mathrm{toSet}}, t^{\\mathrm{toSet}}) = (\\operatorname{Finset.hasSups.sups} \n s t).toSet $$$

Lean4

@[simp, norm_cast]
theorem coe_sups : (↑(s ⊻ t) : Set α) = ↑s ⊻ ↑t :=
  coe_image₂ _ _ _

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