# Relating `Finset.biUnion` with lattice operations #

This file shows `Finset.biUnion` could alternatively be defined in terms of `Finset.sup`.

## TODO #

Remove `Finset.biUnion` in favour of `Finset.sup`.

source
@[simp]
theorem Finset.sup_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : β → α} [SemilatticeSup α] [OrderBot α] [DecidableEq β] (s : Finset γ) (t : γ → Finset β) :
(s.biUnion t).sup f = s.sup fun (x : γ) => (t x).sup f
source
@[simp]
theorem Finset.inf_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : β → α} [SemilatticeInf α] [OrderTop α] [DecidableEq β] (s : Finset γ) (t : γ → Finset β) :
(s.biUnion t).inf f = s.inf fun (x : γ) => (t x).inf f
source
theorem Finset.sup'_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] (f : β → α) [DecidableEq β] {s : Finset γ} (Hs : s.Nonempty) {t : γ → Finset β} (Ht : ∀ (b : γ), (t b).Nonempty) :
(s.biUnion t).sup' ⋯ f = s.sup' Hs fun (b : γ) => (t b).sup' ⋯ f
source
theorem Finset.inf'_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] (f : β → α) [DecidableEq β] {s : Finset γ} (Hs : s.Nonempty) {t : γ → Finset β} (Ht : ∀ (b : γ), (t b).Nonempty) :
(s.biUnion t).inf' ⋯ f = s.inf' Hs fun (b : γ) => (t b).inf' ⋯ f
source
theorem Finset.sup_eq_biUnion {α : Type u_7} {β : Type u_8} [DecidableEq β] (s : Finset α) (t : α → Finset β) :
s.sup t = s.biUnion t