Documentation

Mathlib.Data.Finset.Union

Unions of finite sets #

This file defines the union of a family t : α → Finset β of finsets bounded by a finset s : Finset α.

Main declarations #

TODO #

Remove Finset.biUnion in favour of Finset.sup.

def Finset.disjiUnion {α : Type u_1} {β : Type u_2} (s : Finset α) (t : αFinset β) (hf : (↑s).PairwiseDisjoint t) :

disjiUnion s f h is the set such that a ∈ disjiUnion s f iff a ∈ f i for some i ∈ s. It is the same as s.biUnion f, but it does not require decidable equality on the type. The hypothesis ensures that the sets are disjoint.

Equations
  • s.disjiUnion t hf = { val := s.val.bind (Finset.val t), nodup := }
Instances For
    @[simp]
    theorem Finset.disjiUnion_val {α : Type u_1} {β : Type u_2} (s : Finset α) (t : αFinset β) (h : (↑s).PairwiseDisjoint t) :
    (s.disjiUnion t h).val = s.val.bind fun (a : α) => (t a).val
    @[simp]
    theorem Finset.disjiUnion_empty {α : Type u_1} {β : Type u_2} (t : αFinset β) :
    .disjiUnion t =
    @[simp]
    theorem Finset.mem_disjiUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {t : αFinset β} {b : β} {h : (↑s).PairwiseDisjoint t} :
    b s.disjiUnion t h as, b t a
    @[simp]
    theorem Finset.coe_disjiUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {t : αFinset β} {h : (↑s).PairwiseDisjoint t} :
    (s.disjiUnion t h) = xs, (t x)
    @[simp]
    theorem Finset.disjiUnion_cons {α : Type u_1} {β : Type u_2} (a : α) (s : Finset α) (ha : as) (f : αFinset β) (H : (↑(Finset.cons a s ha)).PairwiseDisjoint f) :
    (Finset.cons a s ha).disjiUnion f H = (f a).disjUnion (s.disjiUnion f )
    @[simp]
    theorem Finset.singleton_disjiUnion {α : Type u_1} {β : Type u_2} {t : αFinset β} (a : α) {h : (↑{a}).PairwiseDisjoint t} :
    {a}.disjiUnion t h = t a
    theorem Finset.disjiUnion_disjiUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Finset α) (f : αFinset β) (g : βFinset γ) (h1 : (↑s).PairwiseDisjoint f) (h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g) :
    (s.disjiUnion f h1).disjiUnion g h2 = s.attach.disjiUnion (fun (a : { x : α // x s }) => (f a).disjiUnion g )
    @[simp]
    theorem Finset.disjiUnion_filter_eq {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (t : Finset β) (f : αβ) :
    t.disjiUnion (fun (a : β) => Finset.filter (fun (x : α) => f x = a) s) = Finset.filter (fun (c : α) => f c t) s
    theorem Finset.disjiUnion_filter_eq_of_maps_to {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : Finset β} {f : αβ} (h : xs, f x t) :
    t.disjiUnion (fun (a : β) => Finset.filter (fun (x : α) => f x = a) s) = s
    def Finset.biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (t : αFinset β) :

    Finset.biUnion s t is the union of t a over a ∈ s.

    (This was formerly bind due to the monad structure on types with DecidableEq.)

    Equations
    • s.biUnion t = (s.val.bind fun (a : α) => (t a).val).toFinset
    Instances For
      @[simp]
      theorem Finset.biUnion_val {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (t : αFinset β) :
      (s.biUnion t).val = (s.val.bind fun (a : α) => (t a).val).dedup
      @[simp]
      theorem Finset.biUnion_empty {α : Type u_1} {β : Type u_2} {t : αFinset β} [DecidableEq β] :
      .biUnion t =
      @[simp]
      theorem Finset.mem_biUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {t : αFinset β} [DecidableEq β] {b : β} :
      b s.biUnion t as, b t a
      @[simp]
      theorem Finset.coe_biUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {t : αFinset β} [DecidableEq β] :
      (s.biUnion t) = xs, (t x)
      @[simp]
      theorem Finset.biUnion_insert {α : Type u_1} {β : Type u_2} {s : Finset α} {t : αFinset β} [DecidableEq β] [DecidableEq α] {a : α} :
      (insert a s).biUnion t = t a s.biUnion t
      theorem Finset.biUnion_congr {α : Type u_1} {β : Type u_2} {s₁ : Finset α} {s₂ : Finset α} {t₁ : αFinset β} {t₂ : αFinset β} [DecidableEq β] (hs : s₁ = s₂) (ht : as₁, t₁ a = t₂ a) :
      s₁.biUnion t₁ = s₂.biUnion t₂
      @[simp]
      theorem Finset.disjiUnion_eq_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : αFinset β) (hf : (↑s).PairwiseDisjoint f) :
      s.disjiUnion f hf = s.biUnion f
      theorem Finset.biUnion_subset {α : Type u_1} {β : Type u_2} {s : Finset α} {t : αFinset β} [DecidableEq β] {s' : Finset β} :
      s.biUnion t s' xs, t x s'
      @[simp]
      theorem Finset.singleton_biUnion {α : Type u_1} {β : Type u_2} {t : αFinset β} [DecidableEq β] {a : α} :
      {a}.biUnion t = t a
      theorem Finset.biUnion_inter {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : αFinset β) (t : Finset β) :
      s.biUnion f t = s.biUnion fun (x : α) => f x t
      theorem Finset.inter_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (t : Finset β) (s : Finset α) (f : αFinset β) :
      t s.biUnion f = s.biUnion fun (x : α) => t f x
      theorem Finset.biUnion_biUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] (s : Finset α) (f : αFinset β) (g : βFinset γ) :
      (s.biUnion f).biUnion g = s.biUnion fun (a : α) => (f a).biUnion g
      theorem Finset.bind_toFinset {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (s : Multiset α) (t : αMultiset β) :
      (s.bind t).toFinset = s.toFinset.biUnion fun (a : α) => (t a).toFinset
      theorem Finset.biUnion_mono {α : Type u_1} {β : Type u_2} {s : Finset α} {t₁ : αFinset β} {t₂ : αFinset β} [DecidableEq β] (h : as, t₁ a t₂ a) :
      s.biUnion t₁ s.biUnion t₂
      theorem Finset.biUnion_subset_biUnion_of_subset_left {α : Type u_1} {β : Type u_2} {s₁ : Finset α} {s₂ : Finset α} [DecidableEq β] (t : αFinset β) (h : s₁ s₂) :
      s₁.biUnion t s₂.biUnion t
      theorem Finset.subset_biUnion_of_mem {α : Type u_1} {β : Type u_2} {s : Finset α} [DecidableEq β] (u : αFinset β) {x : α} (xs : x s) :
      u x s.biUnion u
      @[simp]
      theorem Finset.biUnion_subset_iff_forall_subset {α : Type u_4} {β : Type u_5} [DecidableEq β] {s : Finset α} {t : Finset β} {f : αFinset β} :
      s.biUnion f t xs, f x t
      @[simp]
      theorem Finset.biUnion_singleton_eq_self {α : Type u_1} {s : Finset α} [DecidableEq α] :
      s.biUnion singleton = s
      theorem Finset.filter_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : αFinset β) (p : βProp) [DecidablePred p] :
      Finset.filter p (s.biUnion f) = s.biUnion fun (a : α) => Finset.filter p (f a)
      theorem Finset.biUnion_filter_eq_of_maps_to {α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {s : Finset α} {t : Finset β} {f : αβ} (h : xs, f x t) :
      (t.biUnion fun (a : β) => Finset.filter (fun (c : α) => f c = a) s) = s
      theorem Finset.erase_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : αFinset β) (s : Finset α) (b : β) :
      (s.biUnion f).erase b = s.biUnion fun (x : α) => (f x).erase b
      @[simp]
      theorem Finset.biUnion_nonempty {α : Type u_1} {β : Type u_2} {s : Finset α} {t : αFinset β} [DecidableEq β] :
      (s.biUnion t).Nonempty xs, (t x).Nonempty
      theorem Finset.Nonempty.biUnion {α : Type u_1} {β : Type u_2} {s : Finset α} {t : αFinset β} [DecidableEq β] (hs : s.Nonempty) (ht : xs, (t x).Nonempty) :
      (s.biUnion t).Nonempty
      theorem Finset.disjoint_biUnion_left {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : αFinset β) (t : Finset β) :
      Disjoint (s.biUnion f) t is, Disjoint (f i) t
      theorem Finset.disjoint_biUnion_right {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset β) (t : Finset α) (f : αFinset β) :
      Disjoint s (t.biUnion f) it, Disjoint s (f i)