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.

@[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

@[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

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

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

theorem Finset.sup_eq_biUnion {α : Type u_7} {β : Type u_8} [DecidableEq β] (s : Finset α) (t : α → Finset β) : s.sup t = s.biUnion t