sup_eq_biUnion — Mathlib

English

Let α be a distributive lattice and β a type. For any finite s ⊆ α and t : α → Finset β with DecidableEq β, we have\n\\[ s.sup t = s.biUnion t. \\]

Русский

Пусть α распределённая решётка и β произвольная множ. Для любого конечного s ⊆ α и функции t : α → Finset β с DecidableEq β верно\n\\[ s.sup t = s.biUnion t. \\]

LaTeX

$$$$ \\sup_{x\\in s} t(x) = \\bigcup_{x\\in s} t(x). $$$$

Lean4

theorem sup_eq_biUnion {α β} [DecidableEq β] (s : Finset α) (t : α → Finset β) : s.sup t = s.biUnion t :=
  by
  ext
  rw [mem_sup, mem_biUnion]

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