Documentation

Mathlib.Data.Finset.Lattice

Lattice operations on finsets #

sup #

def Finset.sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : βα) :
α

Supremum of a finite set: sup {a, b, c} f = f a ⊔ f b ⊔ f c

Equations
Instances For
    theorem Finset.sup_def {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : βα} :
    s.sup f = (Multiset.map f s.val).sup
    @[simp]
    theorem Finset.sup_empty {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {f : βα} :
    .sup f =
    @[simp]
    theorem Finset.sup_cons {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : βα} {b : β} (h : bs) :
    (Finset.cons b s h).sup f = f b s.sup f
    @[simp]
    theorem Finset.sup_insert {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : βα} [DecidableEq β] {b : β} :
    (insert b s).sup f = f b s.sup f
    @[simp]
    theorem Finset.sup_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] [DecidableEq β] (s : Finset γ) (f : γβ) (g : βα) :
    (Finset.image f s).sup g = s.sup (g f)
    @[simp]
    theorem Finset.sup_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] (s : Finset γ) (f : γ β) (g : βα) :
    (Finset.map f s).sup g = s.sup (g f)
    @[simp]
    theorem Finset.sup_singleton {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {f : βα} {b : β} :
    {b}.sup f = f b
    theorem Finset.sup_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : βα} {g : βα} :
    s.sup (f g) = s.sup f s.sup g
    theorem Finset.sup_congr {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} {g : βα} (hs : s₁ = s₂) (hfg : as₂, f a = g a) :
    s₁.sup f = s₂.sup g
    @[simp]
    theorem map_finset_sup {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [SemilatticeSup α] [OrderBot α] [SemilatticeSup β] [OrderBot β] [FunLike F α β] [SupBotHomClass F α β] (f : F) (s : Finset ι) (g : ια) :
    f (s.sup g) = s.sup (f g)
    @[simp]
    theorem Finset.sup_le_iff {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : βα} {a : α} :
    s.sup f a bs, f b a
    theorem Finset.sup_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : βα} {a : α} :
    (bs, f b a)s.sup f a

    Alias of the reverse direction of Finset.sup_le_iff.

    theorem Finset.sup_const_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {a : α} :
    (s.sup fun (x : β) => a) a
    theorem Finset.le_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : βα} {b : β} (hb : b s) :
    f b s.sup f
    theorem Finset.le_sup_of_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : βα} {a : α} {b : β} (hb : b s) (h : a f b) :
    a s.sup f
    theorem Finset.sup_union {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} [DecidableEq β] :
    (s₁ s₂).sup f = s₁.sup f s₂.sup f
    @[simp]
    theorem Finset.sup_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] {f : βα} [DecidableEq β] (s : Finset γ) (t : γFinset β) :
    (s.biUnion t).sup f = s.sup fun (x : γ) => (t x).sup f
    theorem Finset.sup_const {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (h : s.Nonempty) (c : α) :
    (s.sup fun (x : β) => c) = c
    @[simp]
    theorem Finset.sup_bot {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) :
    (s.sup fun (x : β) => ) =
    theorem Finset.sup_ite {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : βα} {g : βα} (p : βProp) [DecidablePred p] :
    (s.sup fun (i : β) => if p i then f i else g i) = (Finset.filter p s).sup f (Finset.filter (fun (i : β) => ¬p i) s).sup g
    theorem Finset.sup_mono_fun {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : βα} {g : βα} (h : bs, f b g b) :
    s.sup f s.sup g
    theorem Finset.sup_mono {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} (h : s₁ s₂) :
    s₁.sup f s₂.sup f
    theorem Finset.sup_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] (s : Finset β) (t : Finset γ) (f : βγα) :
    (s.sup fun (b : β) => t.sup (f b)) = t.sup fun (c : γ) => s.sup fun (b : β) => f b c
    @[simp]
    theorem Finset.sup_attach {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : βα) :
    (s.attach.sup fun (x : { x : β // x s }) => f x) = s.sup f
    theorem Finset.sup_product_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] (s : Finset β) (t : Finset γ) (f : β × γα) :
    (s ×ˢ t).sup f = s.sup fun (i : β) => t.sup fun (i' : γ) => f (i, i')

    See also Finset.product_biUnion.

    theorem Finset.sup_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] (s : Finset β) (t : Finset γ) (f : β × γα) :
    (s ×ˢ t).sup f = t.sup fun (i' : γ) => s.sup fun (i : β) => f (i, i')
    @[simp]
    theorem Finset.sup_prodMap {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeSup α] [SemilatticeSup β] [OrderBot α] [OrderBot β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ια) (g : κβ) :
    (s ×ˢ t).sup (Prod.map f g) = (s.sup f, t.sup g)
    @[simp]
    theorem Finset.sup_erase_bot {α : Type u_2} [SemilatticeSup α] [OrderBot α] [DecidableEq α] (s : Finset α) :
    (s.erase ).sup id = s.sup id
    theorem Finset.sup_sdiff_right {α : Type u_7} {β : Type u_8} [GeneralizedBooleanAlgebra α] (s : Finset β) (f : βα) (a : α) :
    (s.sup fun (b : β) => f b \ a) = s.sup f \ a
    theorem Finset.comp_sup_eq_sup_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [OrderBot α] [SemilatticeSup γ] [OrderBot γ] {s : Finset β} {f : βα} (g : αγ) (g_sup : ∀ (x y : α), g (x y) = g x g y) (bot : g = ) :
    g (s.sup f) = s.sup (g f)
    theorem Finset.sup_coe {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {P : αProp} {Pbot : P } {Psup : ∀ ⦃x y : α⦄, P xP yP (x y)} (t : Finset β) (f : β{ x : α // P x }) :
    (t.sup f) = t.sup fun (x : β) => (f x)

    Computing sup in a subtype (closed under sup) is the same as computing it in α.

    @[simp]
    theorem Finset.sup_toFinset {α : Type u_7} {β : Type u_8} [DecidableEq β] (s : Finset α) (f : αMultiset β) :
    (s.sup f).toFinset = s.sup fun (x : α) => (f x).toFinset
    theorem List.foldr_sup_eq_sup_toFinset {α : Type u_2} [SemilatticeSup α] [OrderBot α] [DecidableEq α] (l : List α) :
    List.foldr (fun (x x_1 : α) => x x_1) l = l.toFinset.sup id
    theorem Finset.sup_induction {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : βα} {p : αProp} (hb : p ) (hp : ∀ (a₁ : α), p a₁∀ (a₂ : α), p a₂p (a₁ a₂)) (hs : bs, p (f b)) :
    p (s.sup f)
    theorem Finset.sup_le_of_le_directed {α : Type u_7} [SemilatticeSup α] [OrderBot α] (s : Set α) (hs : s.Nonempty) (hdir : DirectedOn (fun (x x_1 : α) => x x_1) s) (t : Finset α) :
    (xt, ys, x y)xs, t.sup id x
    theorem Finset.sup_mem {α : Type u_2} [SemilatticeSup α] [OrderBot α] (s : Set α) (w₁ : s) (w₂ : xs, ys, x y s) {ι : Type u_7} (t : Finset ι) (p : ια) (h : it, p i s) :
    t.sup p s
    @[simp]
    theorem Finset.sup_eq_bot_iff {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (f : βα) (S : Finset β) :
    S.sup f = sS, f s =
    theorem Finset.sup_eq_iSup {α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : αβ) :
    s.sup f = as, f a
    theorem Finset.sup_id_eq_sSup {α : Type u_2} [CompleteLattice α] (s : Finset α) :
    s.sup id = sSup s
    theorem Finset.sup_id_set_eq_sUnion {α : Type u_2} (s : Finset (Set α)) :
    s.sup id = ⋃₀ s
    @[simp]
    theorem Finset.sup_set_eq_biUnion {α : Type u_2} {β : Type u_3} (s : Finset α) (f : αSet β) :
    s.sup f = xs, f x
    theorem Finset.sup_eq_sSup_image {α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : αβ) :
    s.sup f = sSup (f '' s)

    inf #

    def Finset.inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : βα) :
    α

    Infimum of a finite set: inf {a, b, c} f = f a ⊓ f b ⊓ f c

    Equations
    Instances For
      theorem Finset.inf_def {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : βα} :
      s.inf f = (Multiset.map f s.val).inf
      @[simp]
      theorem Finset.inf_empty {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {f : βα} :
      .inf f =
      @[simp]
      theorem Finset.inf_cons {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : βα} {b : β} (h : bs) :
      (Finset.cons b s h).inf f = f b s.inf f
      @[simp]
      theorem Finset.inf_insert {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : βα} [DecidableEq β] {b : β} :
      (insert b s).inf f = f b s.inf f
      @[simp]
      theorem Finset.inf_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] [DecidableEq β] (s : Finset γ) (f : γβ) (g : βα) :
      (Finset.image f s).inf g = s.inf (g f)
      @[simp]
      theorem Finset.inf_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] (s : Finset γ) (f : γ β) (g : βα) :
      (Finset.map f s).inf g = s.inf (g f)
      @[simp]
      theorem Finset.inf_singleton {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {f : βα} {b : β} :
      {b}.inf f = f b
      theorem Finset.inf_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : βα} {g : βα} :
      s.inf (f g) = s.inf f s.inf g
      theorem Finset.inf_congr {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} {g : βα} (hs : s₁ = s₂) (hfg : as₂, f a = g a) :
      s₁.inf f = s₂.inf g
      @[simp]
      theorem map_finset_inf {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [SemilatticeInf α] [OrderTop α] [SemilatticeInf β] [OrderTop β] [FunLike F α β] [InfTopHomClass F α β] (f : F) (s : Finset ι) (g : ια) :
      f (s.inf g) = s.inf (f g)
      @[simp]
      theorem Finset.le_inf_iff {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : βα} {a : α} :
      a s.inf f bs, a f b
      theorem Finset.le_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : βα} {a : α} :
      (bs, a f b)a s.inf f

      Alias of the reverse direction of Finset.le_inf_iff.

      theorem Finset.le_inf_const_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {a : α} :
      a s.inf fun (x : β) => a
      theorem Finset.inf_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : βα} {b : β} (hb : b s) :
      s.inf f f b
      theorem Finset.inf_le_of_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : βα} {a : α} {b : β} (hb : b s) (h : f b a) :
      s.inf f a
      theorem Finset.inf_union {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} [DecidableEq β] :
      (s₁ s₂).inf f = s₁.inf f s₂.inf f
      @[simp]
      theorem Finset.inf_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] {f : βα} [DecidableEq β] (s : Finset γ) (t : γFinset β) :
      (s.biUnion t).inf f = s.inf fun (x : γ) => (t x).inf f
      theorem Finset.inf_const {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} (h : s.Nonempty) (c : α) :
      (s.inf fun (x : β) => c) = c
      @[simp]
      theorem Finset.inf_top {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) :
      (s.inf fun (x : β) => ) =
      theorem Finset.inf_ite {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : βα} {g : βα} (p : βProp) [DecidablePred p] :
      (s.inf fun (i : β) => if p i then f i else g i) = (Finset.filter p s).inf f (Finset.filter (fun (i : β) => ¬p i) s).inf g
      theorem Finset.inf_mono_fun {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : βα} {g : βα} (h : bs, f b g b) :
      s.inf f s.inf g
      theorem Finset.inf_mono {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s₁ : Finset β} {s₂ : Finset β} {f : βα} (h : s₁ s₂) :
      s₂.inf f s₁.inf f
      theorem Finset.inf_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] (s : Finset β) (t : Finset γ) (f : βγα) :
      (s.inf fun (b : β) => t.inf (f b)) = t.inf fun (c : γ) => s.inf fun (b : β) => f b c
      theorem Finset.inf_attach {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : βα) :
      (s.attach.inf fun (x : { x : β // x s }) => f x) = s.inf f
      theorem Finset.inf_product_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] (s : Finset β) (t : Finset γ) (f : β × γα) :
      (s ×ˢ t).inf f = s.inf fun (i : β) => t.inf fun (i' : γ) => f (i, i')
      theorem Finset.inf_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] (s : Finset β) (t : Finset γ) (f : β × γα) :
      (s ×ˢ t).inf f = t.inf fun (i' : γ) => s.inf fun (i : β) => f (i, i')
      @[simp]
      theorem Finset.inf_prodMap {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeInf α] [SemilatticeInf β] [OrderTop α] [OrderTop β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ια) (g : κβ) :
      (s ×ˢ t).inf (Prod.map f g) = (s.inf f, t.inf g)
      @[simp]
      theorem Finset.inf_erase_top {α : Type u_2} [SemilatticeInf α] [OrderTop α] [DecidableEq α] (s : Finset α) :
      (s.erase ).inf id = s.inf id
      theorem Finset.comp_inf_eq_inf_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [OrderTop α] [SemilatticeInf γ] [OrderTop γ] {s : Finset β} {f : βα} (g : αγ) (g_inf : ∀ (x y : α), g (x y) = g x g y) (top : g = ) :
      g (s.inf f) = s.inf (g f)
      theorem Finset.inf_coe {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {P : αProp} {Ptop : P } {Pinf : ∀ ⦃x y : α⦄, P xP yP (x y)} (t : Finset β) (f : β{ x : α // P x }) :
      (t.inf f) = t.inf fun (x : β) => (f x)

      Computing inf in a subtype (closed under inf) is the same as computing it in α.

      theorem List.foldr_inf_eq_inf_toFinset {α : Type u_2} [SemilatticeInf α] [OrderTop α] [DecidableEq α] (l : List α) :
      List.foldr (fun (x x_1 : α) => x x_1) l = l.toFinset.inf id
      theorem Finset.inf_induction {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} {f : βα} {p : αProp} (ht : p ) (hp : ∀ (a₁ : α), p a₁∀ (a₂ : α), p a₂p (a₁ a₂)) (hs : bs, p (f b)) :
      p (s.inf f)
      theorem Finset.inf_mem {α : Type u_2} [SemilatticeInf α] [OrderTop α] (s : Set α) (w₁ : s) (w₂ : xs, ys, x y s) {ι : Type u_7} (t : Finset ι) (p : ια) (h : it, p i s) :
      t.inf p s
      @[simp]
      theorem Finset.inf_eq_top_iff {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (f : βα) (S : Finset β) :
      S.inf f = sS, f s =
      @[simp]
      theorem Finset.toDual_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : βα) :
      OrderDual.toDual (s.sup f) = s.inf (OrderDual.toDual f)
      @[simp]
      theorem Finset.toDual_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : βα) :
      OrderDual.toDual (s.inf f) = s.sup (OrderDual.toDual f)
      @[simp]
      theorem Finset.ofDual_sup {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : βαᵒᵈ) :
      OrderDual.ofDual (s.sup f) = s.inf (OrderDual.ofDual f)
      @[simp]
      theorem Finset.ofDual_inf {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : βαᵒᵈ) :
      OrderDual.ofDual (s.inf f) = s.sup (OrderDual.ofDual f)
      theorem Finset.sup_inf_distrib_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] (s : Finset ι) (f : ια) (a : α) :
      a s.sup f = s.sup fun (i : ι) => a f i
      theorem Finset.sup_inf_distrib_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] (s : Finset ι) (f : ια) (a : α) :
      s.sup f a = s.sup fun (i : ι) => f i a
      theorem Finset.disjoint_sup_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ια} {a : α} :
      Disjoint a (s.sup f) ∀ ⦃i : ι⦄, i sDisjoint a (f i)
      theorem Finset.disjoint_sup_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderBot α] {s : Finset ι} {f : ια} {a : α} :
      Disjoint (s.sup f) a ∀ ⦃i : ι⦄, i sDisjoint (f i) a
      theorem Finset.sup_inf_sup {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [DistribLattice α] [OrderBot α] (s : Finset ι) (t : Finset κ) (f : ια) (g : κα) :
      s.sup f t.sup g = (s ×ˢ t).sup fun (i : ι × κ) => f i.1 g i.2
      theorem Finset.inf_sup_distrib_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderTop α] (s : Finset ι) (f : ια) (a : α) :
      a s.inf f = s.inf fun (i : ι) => a f i
      theorem Finset.inf_sup_distrib_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderTop α] (s : Finset ι) (f : ια) (a : α) :
      s.inf f a = s.inf fun (i : ι) => f i a
      theorem Finset.codisjoint_inf_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderTop α] {f : ια} {s : Finset ι} {a : α} :
      Codisjoint a (s.inf f) ∀ ⦃i : ι⦄, i sCodisjoint a (f i)
      theorem Finset.codisjoint_inf_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] [OrderTop α] {f : ια} {s : Finset ι} {a : α} :
      Codisjoint (s.inf f) a ∀ ⦃i : ι⦄, i sCodisjoint (f i) a
      theorem Finset.inf_sup_inf {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [DistribLattice α] [OrderTop α] (s : Finset ι) (t : Finset κ) (f : ια) (g : κα) :
      s.inf f t.inf g = (s ×ˢ t).inf fun (i : ι × κ) => f i.1 g i.2
      theorem Finset.inf_sup {α : Type u_2} {ι : Type u_5} [DistribLattice α] [BoundedOrder α] [DecidableEq ι] {κ : ιType u_7} (s : Finset ι) (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ iα) :
      (s.inf fun (i : ι) => (t i).sup (f i)) = (s.pi t).sup fun (g : (a : ι) → a sκ a) => s.attach.inf fun (i : { x : ι // x s }) => f (i) (g i )
      theorem Finset.sup_inf {α : Type u_2} {ι : Type u_5} [DistribLattice α] [BoundedOrder α] [DecidableEq ι] {κ : ιType u_7} (s : Finset ι) (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ iα) :
      (s.sup fun (i : ι) => (t i).inf (f i)) = (s.pi t).inf fun (g : (a : ι) → a sκ a) => s.attach.sup fun (i : { x : ι // x s }) => f (i) (g i )
      theorem Finset.sup_sdiff_left {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ια) (a : α) :
      (s.sup fun (b : ι) => a \ f b) = a \ s.inf f
      theorem Finset.inf_sdiff_left {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ια) (a : α) :
      (s.inf fun (b : ι) => a \ f b) = a \ s.sup f
      theorem Finset.inf_sdiff_right {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ια) (a : α) :
      (s.inf fun (b : ι) => f b \ a) = s.inf f \ a
      theorem Finset.inf_himp_right {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ια) (a : α) :
      (s.inf fun (b : ι) => f b a) = s.sup f a
      theorem Finset.sup_himp_right {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ια) (a : α) :
      (s.sup fun (b : ι) => f b a) = s.inf f a
      theorem Finset.sup_himp_left {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] {s : Finset ι} (hs : s.Nonempty) (f : ια) (a : α) :
      (s.sup fun (b : ι) => a f b) = a s.sup f
      @[simp]
      theorem Finset.compl_sup {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ια) :
      (s.sup f) = s.inf fun (i : ι) => (f i)
      @[simp]
      theorem Finset.compl_inf {α : Type u_2} {ι : Type u_5} [BooleanAlgebra α] (s : Finset ι) (f : ια) :
      (s.inf f) = s.sup fun (i : ι) => (f i)
      theorem Finset.comp_sup_eq_sup_comp_of_is_total {α : Type u_2} {β : Type u_3} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ια} [SemilatticeSup β] [OrderBot β] (g : αβ) (mono_g : Monotone g) (bot : g = ) :
      g (s.sup f) = s.sup (g f)
      @[simp]
      theorem Finset.le_sup_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ια} {a : α} (ha : < a) :
      a s.sup f bs, a f b
      theorem Finset.sup_eq_top_iff {ι : Type u_5} {α : Type u_7} [LinearOrder α] [BoundedOrder α] [Nontrivial α] {s : Finset ι} {f : ια} :
      s.sup f = bs, f b =
      theorem Finset.Nonempty.sup_eq_top_iff {ι : Type u_5} {α : Type u_7} [LinearOrder α] [BoundedOrder α] {s : Finset ι} {f : ια} (hs : s.Nonempty) :
      s.sup f = bs, f b =
      @[simp]
      theorem Finset.lt_sup_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ια} {a : α} :
      a < s.sup f bs, a < f b
      @[simp]
      theorem Finset.sup_lt_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] {s : Finset ι} {f : ια} {a : α} (ha : < a) :
      s.sup f < a bs, f b < a
      theorem Finset.comp_inf_eq_inf_comp_of_is_total {α : Type u_2} {β : Type u_3} {ι : Type u_5} [LinearOrder α] [OrderTop α] {s : Finset ι} {f : ια} [SemilatticeInf β] [OrderTop β] (g : αβ) (mono_g : Monotone g) (top : g = ) :
      g (s.inf f) = s.inf (g f)
      @[simp]
      theorem Finset.inf_le_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderTop α] {s : Finset ι} {f : ια} {a : α} (ha : a < ) :
      s.inf f a bs, f b a
      theorem Finset.inf_eq_bot_iff {ι : Type u_5} {α : Type u_7} [LinearOrder α] [BoundedOrder α] [Nontrivial α] {s : Finset ι} {f : ια} :
      s.inf f = bs, f b =
      theorem Finset.Nonempty.inf_eq_bot_iff {ι : Type u_5} {α : Type u_7} [LinearOrder α] [BoundedOrder α] {s : Finset ι} {f : ια} (h : s.Nonempty) :
      s.inf f = bs, f b =
      @[simp]
      theorem Finset.inf_lt_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderTop α] {s : Finset ι} {f : ια} {a : α} :
      s.inf f < a bs, f b < a
      @[simp]
      theorem Finset.lt_inf_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderTop α] {s : Finset ι} {f : ια} {a : α} (ha : a < ) :
      a < s.inf f bs, a < f b
      theorem Finset.inf_eq_iInf {α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : αβ) :
      s.inf f = as, f a
      theorem Finset.inf_id_eq_sInf {α : Type u_2} [CompleteLattice α] (s : Finset α) :
      s.inf id = sInf s
      theorem Finset.inf_id_set_eq_sInter {α : Type u_2} (s : Finset (Set α)) :
      s.inf id = ⋂₀ s
      @[simp]
      theorem Finset.inf_set_eq_iInter {α : Type u_2} {β : Type u_3} (s : Finset α) (f : αSet β) :
      s.inf f = xs, f x
      theorem Finset.inf_eq_sInf_image {α : Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset α) (f : αβ) :
      s.inf f = sInf (f '' s)
      theorem Finset.sup_of_mem {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (f : βα) {b : β} (h : b s) :
      ∃ (a : α), s.sup (WithBot.some f) = a
      def Finset.sup' {α : Type u_2} {β : Type u_3} [SemilatticeSup α] (s : Finset β) (H : s.Nonempty) (f : βα) :
      α

      Given nonempty finset s then s.sup' H f is the supremum of its image under f in (possibly unbounded) join-semilattice α, where H is a proof of nonemptiness. If α has a bottom element you may instead use Finset.sup which does not require s nonempty.

      Equations
      • s.sup' H f = (s.sup (WithBot.some f)).unbot
      Instances For
        @[simp]
        theorem Finset.coe_sup' {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : βα) :
        (s.sup' H f) = s.sup (WithBot.some f)
        @[simp]
        theorem Finset.sup'_cons {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : βα) {b : β} {hb : bs} :
        (Finset.cons b s hb).sup' f = f b s.sup' H f
        @[simp]
        theorem Finset.sup'_insert {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : βα) [DecidableEq β] {b : β} :
        (insert b s).sup' f = f b s.sup' H f
        @[simp]
        theorem Finset.sup'_singleton {α : Type u_2} {β : Type u_3} [SemilatticeSup α] (f : βα) {b : β} :
        {b}.sup' f = f b
        @[simp]
        theorem Finset.sup'_le_iff {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : βα) {a : α} :
        s.sup' H f a bs, f b a
        theorem Finset.sup'_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : βα) {a : α} :
        (bs, f b a)s.sup' H f a

        Alias of the reverse direction of Finset.sup'_le_iff.

        theorem Finset.le_sup' {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (f : βα) {b : β} (h : b s) :
        f b s.sup' f
        theorem Finset.le_sup'_of_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (f : βα) {a : α} {b : β} (hb : b s) (h : a f b) :
        a s.sup' f
        @[simp]
        theorem Finset.sup'_const {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (a : α) :
        (s.sup' H fun (x : β) => a) = a
        theorem Finset.sup'_union {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [DecidableEq β] {s₁ : Finset β} {s₂ : Finset β} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) (f : βα) :
        (s₁ s₂).sup' f = s₁.sup' h₁ f s₂.sup' h₂ 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.sup'_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] {s : Finset β} {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty) (f : βγα) :
        (s.sup' hs fun (b : β) => t.sup' ht (f b)) = t.sup' ht fun (c : γ) => s.sup' hs fun (b : β) => f b c
        theorem Finset.sup'_product_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] {s : Finset β} {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γα) :
        (s ×ˢ t).sup' h f = s.sup' fun (i : β) => t.sup' fun (i' : γ) => f (i, i')
        theorem Finset.sup'_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] {s : Finset β} {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γα) :
        (s ×ˢ t).sup' h f = t.sup' fun (i' : γ) => s.sup' fun (i : β) => f (i, i')
        theorem Finset.prodMk_sup'_sup' {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeSup α] [SemilatticeSup β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ια) (g : κβ) :
        (s.sup' hs f, t.sup' ht g) = (s ×ˢ t).sup' (Prod.map f g)

        See also Finset.sup'_prodMap.

        theorem Finset.sup'_prodMap {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeSup α] [SemilatticeSup β] {s : Finset ι} {t : Finset κ} (hst : (s ×ˢ t).Nonempty) (f : ια) (g : κβ) :
        (s ×ˢ t).sup' hst (Prod.map f g) = (s.sup' f, t.sup' g)

        See also Finset.prodMk_sup'_sup'.

        theorem Finset.sup'_induction {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : βα) {p : αProp} (hp : ∀ (a₁ : α), p a₁∀ (a₂ : α), p a₂p (a₁ a₂)) (hs : bs, p (f b)) :
        p (s.sup' H f)
        theorem Finset.sup'_mem {α : Type u_2} [SemilatticeSup α] (s : Set α) (w : xs, ys, x y s) {ι : Type u_7} (t : Finset ι) (H : t.Nonempty) (p : ια) (h : it, p i s) :
        t.sup' H p s
        theorem Finset.sup'_congr {α : Type u_2} {β : Type u_3} [SemilatticeSup α] {s : Finset β} (H : s.Nonempty) {t : Finset β} {f : βα} {g : βα} (h₁ : s = t) (h₂ : xs, f x = g x) :
        s.sup' H f = t.sup' g
        theorem Finset.comp_sup'_eq_sup'_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [SemilatticeSup γ] {s : Finset β} (H : s.Nonempty) {f : βα} (g : αγ) (g_sup : ∀ (x y : α), g (x y) = g x g y) :
        g (s.sup' H f) = s.sup' H (g f)
        @[simp]
        theorem map_finset_sup' {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [SemilatticeSup α] [SemilatticeSup β] [FunLike F α β] [SupHomClass F α β] (f : F) {s : Finset ι} (hs : s.Nonempty) (g : ια) :
        f (s.sup' hs g) = s.sup' hs (f g)
        theorem Finset.nsmul_sup' {α : Type u_2} {β : Type u_3} [LinearOrderedAddCommMonoid β] {s : Finset α} (hs : s.Nonempty) (f : αβ) (n : ) :
        (s.sup' hs fun (a : α) => n f a) = n s.sup' hs f
        @[simp]
        theorem Finset.sup'_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [DecidableEq β] {s : Finset γ} {f : γβ} (hs : (Finset.image f s).Nonempty) (g : βα) :
        (Finset.image f s).sup' hs g = s.sup' (g f)

        To rewrite from right to left, use Finset.sup'_comp_eq_image.

        theorem Finset.sup'_comp_eq_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] [DecidableEq β] {s : Finset γ} {f : γβ} (hs : s.Nonempty) (g : βα) :
        s.sup' hs (g f) = (Finset.image f s).sup' g

        A version of Finset.sup'_image with LHS and RHS reversed. Also, this lemma assumes that s is nonempty instead of assuming that its image is nonempty.

        @[simp]
        theorem Finset.sup'_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] {s : Finset γ} {f : γ β} (g : βα) (hs : (Finset.map f s).Nonempty) :
        (Finset.map f s).sup' hs g = s.sup' (g f)

        To rewrite from right to left, use Finset.sup'_comp_eq_map.

        theorem Finset.sup'_comp_eq_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeSup α] {s : Finset γ} {f : γ β} (g : βα) (hs : s.Nonempty) :
        s.sup' hs (g f) = (Finset.map f s).sup' g

        A version of Finset.sup'_map with LHS and RHS reversed. Also, this lemma assumes that s is nonempty instead of assuming that its image is nonempty.

        theorem Finset.sup'_mono {α : Type u_2} {β : Type u_3} [SemilatticeSup α] (f : βα) {s₁ : Finset β} {s₂ : Finset β} (h : s₁ s₂) (h₁ : s₁.Nonempty) :
        s₁.sup' h₁ f s₂.sup' f
        theorem GCongr.finset_sup'_le {α : Type u_2} {β : Type u_3} [SemilatticeSup α] (f : βα) {s₁ : Finset β} {s₂ : Finset β} (h : s₁ s₂) {h₁ : s₁.Nonempty} {h₂ : s₂.Nonempty} :
        s₁.sup' h₁ f s₂.sup' h₂ f

        A version of Finset.sup'_mono acceptable for @[gcongr]. Instead of deducing s₂.Nonempty from s₁.Nonempty and s₁ ⊆ s₂, this version takes it as an argument.

        theorem Finset.inf_of_mem {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (f : βα) {b : β} (h : b s) :
        ∃ (a : α), s.inf (WithTop.some f) = a
        def Finset.inf' {α : Type u_2} {β : Type u_3} [SemilatticeInf α] (s : Finset β) (H : s.Nonempty) (f : βα) :
        α

        Given nonempty finset s then s.inf' H f is the infimum of its image under f in (possibly unbounded) meet-semilattice α, where H is a proof of nonemptiness. If α has a top element you may instead use Finset.inf which does not require s nonempty.

        Equations
        • s.inf' H f = (s.inf (WithTop.some f)).untop
        Instances For
          @[simp]
          theorem Finset.coe_inf' {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : βα) :
          (s.inf' H f) = s.inf (WithTop.some f)
          @[simp]
          theorem Finset.inf'_cons {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : βα) {b : β} {hb : bs} :
          (Finset.cons b s hb).inf' f = f b s.inf' H f
          @[simp]
          theorem Finset.inf'_insert {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : βα) [DecidableEq β] {b : β} :
          (insert b s).inf' f = f b s.inf' H f
          @[simp]
          theorem Finset.inf'_singleton {α : Type u_2} {β : Type u_3} [SemilatticeInf α] (f : βα) {b : β} :
          {b}.inf' f = f b
          @[simp]
          theorem Finset.le_inf'_iff {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : βα) {a : α} :
          a s.inf' H f bs, a f b
          theorem Finset.le_inf' {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : βα) {a : α} (hs : bs, a f b) :
          a s.inf' H f
          theorem Finset.inf'_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (f : βα) {b : β} (h : b s) :
          s.inf' f f b
          theorem Finset.inf'_le_of_le {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (f : βα) {a : α} {b : β} (hb : b s) (h : f b a) :
          s.inf' f a
          @[simp]
          theorem Finset.inf'_const {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (a : α) :
          (s.inf' H fun (x : β) => a) = a
          theorem Finset.inf'_union {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [DecidableEq β] {s₁ : Finset β} {s₂ : Finset β} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) (f : βα) :
          (s₁ s₂).inf' f = s₁.inf' h₁ f s₂.inf' h₂ 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.inf'_comm {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] {s : Finset β} {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty) (f : βγα) :
          (s.inf' hs fun (b : β) => t.inf' ht (f b)) = t.inf' ht fun (c : γ) => s.inf' hs fun (b : β) => f b c
          theorem Finset.inf'_product_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] {s : Finset β} {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γα) :
          (s ×ˢ t).inf' h f = s.inf' fun (i : β) => t.inf' fun (i' : γ) => f (i, i')
          theorem Finset.inf'_product_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] {s : Finset β} {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γα) :
          (s ×ˢ t).inf' h f = t.inf' fun (i' : γ) => s.inf' fun (i : β) => f (i, i')
          theorem Finset.prodMk_inf'_inf' {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeInf α] [SemilatticeInf β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ια) (g : κβ) :
          (s.inf' hs f, t.inf' ht g) = (s ×ˢ t).inf' (Prod.map f g)

          See also Finset.inf'_prodMap.

          theorem Finset.inf'_prodMap {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeInf α] [SemilatticeInf β] {s : Finset ι} {t : Finset κ} (hst : (s ×ˢ t).Nonempty) (f : ια) (g : κβ) :
          (s ×ˢ t).inf' hst (Prod.map f g) = (s.inf' f, t.inf' g)

          See also Finset.prodMk_inf'_inf'.

          theorem Finset.comp_inf'_eq_inf'_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [SemilatticeInf γ] {s : Finset β} (H : s.Nonempty) {f : βα} (g : αγ) (g_inf : ∀ (x y : α), g (x y) = g x g y) :
          g (s.inf' H f) = s.inf' H (g f)
          theorem Finset.inf'_induction {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : βα) {p : αProp} (hp : ∀ (a₁ : α), p a₁∀ (a₂ : α), p a₂p (a₁ a₂)) (hs : bs, p (f b)) :
          p (s.inf' H f)
          theorem Finset.inf'_mem {α : Type u_2} [SemilatticeInf α] (s : Set α) (w : xs, ys, x y s) {ι : Type u_7} (t : Finset ι) (H : t.Nonempty) (p : ια) (h : it, p i s) :
          t.inf' H p s
          theorem Finset.inf'_congr {α : Type u_2} {β : Type u_3} [SemilatticeInf α] {s : Finset β} (H : s.Nonempty) {t : Finset β} {f : βα} {g : βα} (h₁ : s = t) (h₂ : xs, f x = g x) :
          s.inf' H f = t.inf' g
          @[simp]
          theorem map_finset_inf' {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [SemilatticeInf α] [SemilatticeInf β] [FunLike F α β] [InfHomClass F α β] (f : F) {s : Finset ι} (hs : s.Nonempty) (g : ια) :
          f (s.inf' hs g) = s.inf' hs (f g)
          theorem Finset.nsmul_inf' {α : Type u_2} {β : Type u_3} [LinearOrderedAddCommMonoid β] {s : Finset α} (hs : s.Nonempty) (f : αβ) (n : ) :
          (s.inf' hs fun (a : α) => n f a) = n s.inf' hs f
          @[simp]
          theorem Finset.inf'_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [DecidableEq β] {s : Finset γ} {f : γβ} (hs : (Finset.image f s).Nonempty) (g : βα) :
          (Finset.image f s).inf' hs g = s.inf' (g f)

          To rewrite from right to left, use Finset.inf'_comp_eq_image.

          theorem Finset.inf'_comp_eq_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] [DecidableEq β] {s : Finset γ} {f : γβ} (hs : s.Nonempty) (g : βα) :
          s.inf' hs (g f) = (Finset.image f s).inf' g

          A version of Finset.inf'_image with LHS and RHS reversed. Also, this lemma assumes that s is nonempty instead of assuming that its image is nonempty.

          @[simp]
          theorem Finset.inf'_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] {s : Finset γ} {f : γ β} (g : βα) (hs : (Finset.map f s).Nonempty) :
          (Finset.map f s).inf' hs g = s.inf' (g f)

          To rewrite from right to left, use Finset.inf'_comp_eq_map.

          theorem Finset.inf'_comp_eq_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SemilatticeInf α] {s : Finset γ} {f : γ β} (g : βα) (hs : s.Nonempty) :
          s.inf' hs (g f) = (Finset.map f s).inf' g

          A version of Finset.inf'_map with LHS and RHS reversed. Also, this lemma assumes that s is nonempty instead of assuming that its image is nonempty.

          theorem Finset.inf'_mono {α : Type u_2} {β : Type u_3} [SemilatticeInf α] (f : βα) {s₁ : Finset β} {s₂ : Finset β} (h : s₁ s₂) (h₁ : s₁.Nonempty) :
          s₂.inf' f s₁.inf' h₁ f
          theorem GCongr.finset_inf'_mono {α : Type u_2} {β : Type u_3} [SemilatticeInf α] (f : βα) {s₁ : Finset β} {s₂ : Finset β} (h : s₁ s₂) {h₁ : s₁.Nonempty} {h₂ : s₂.Nonempty} :
          s₂.inf' h₂ f s₁.inf' h₁ f

          A version of Finset.inf'_mono acceptable for @[gcongr]. Instead of deducing s₂.Nonempty from s₁.Nonempty and s₁ ⊆ s₂, this version takes it as an argument.

          theorem Finset.sup'_eq_sup {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (H : s.Nonempty) (f : βα) :
          s.sup' H f = s.sup f
          theorem Finset.coe_sup_of_nonempty {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] {s : Finset β} (h : s.Nonempty) (f : βα) :
          (s.sup f) = s.sup (WithBot.some f)
          theorem Finset.inf'_eq_inf {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} (H : s.Nonempty) (f : βα) :
          s.inf' H f = s.inf f
          theorem Finset.coe_inf_of_nonempty {α : Type u_2} {β : Type u_3} [SemilatticeInf α] [OrderTop α] {s : Finset β} (h : s.Nonempty) (f : βα) :
          (s.inf f) = s.inf (WithTop.some f)
          @[simp]
          theorem Finset.sup_apply {α : Type u_2} {β : Type u_3} {C : βType u_7} [(b : β) → SemilatticeSup (C b)] [(b : β) → OrderBot (C b)] (s : Finset α) (f : α(b : β) → C b) (b : β) :
          s.sup f b = s.sup fun (a : α) => f a b
          @[simp]
          theorem Finset.inf_apply {α : Type u_2} {β : Type u_3} {C : βType u_7} [(b : β) → SemilatticeInf (C b)] [(b : β) → OrderTop (C b)] (s : Finset α) (f : α(b : β) → C b) (b : β) :
          s.inf f b = s.inf fun (a : α) => f a b
          @[simp]
          theorem Finset.sup'_apply {α : Type u_2} {β : Type u_3} {C : βType u_7} [(b : β) → SemilatticeSup (C b)] {s : Finset α} (H : s.Nonempty) (f : α(b : β) → C b) (b : β) :
          s.sup' H f b = s.sup' H fun (a : α) => f a b
          @[simp]
          theorem Finset.inf'_apply {α : Type u_2} {β : Type u_3} {C : βType u_7} [(b : β) → SemilatticeInf (C b)] {s : Finset α} (H : s.Nonempty) (f : α(b : β) → C b) (b : β) :
          s.inf' H f b = s.inf' H fun (a : α) => f a b
          @[simp]
          theorem Finset.toDual_sup' {α : Type u_2} {ι : Type u_5} [SemilatticeSup α] {s : Finset ι} (hs : s.Nonempty) (f : ια) :
          OrderDual.toDual (s.sup' hs f) = s.inf' hs (OrderDual.toDual f)
          @[simp]
          theorem Finset.toDual_inf' {α : Type u_2} {ι : Type u_5} [SemilatticeInf α] {s : Finset ι} (hs : s.Nonempty) (f : ια) :
          OrderDual.toDual (s.inf' hs f) = s.sup' hs (OrderDual.toDual f)
          @[simp]
          theorem Finset.ofDual_sup' {α : Type u_2} {ι : Type u_5} [SemilatticeInf α] {s : Finset ι} (hs : s.Nonempty) (f : ιαᵒᵈ) :
          OrderDual.ofDual (s.sup' hs f) = s.inf' hs (OrderDual.ofDual f)
          @[simp]
          theorem Finset.ofDual_inf' {α : Type u_2} {ι : Type u_5} [SemilatticeSup α] {s : Finset ι} (hs : s.Nonempty) (f : ιαᵒᵈ) :
          OrderDual.ofDual (s.inf' hs f) = s.sup' hs (OrderDual.ofDual f)
          theorem Finset.sup'_inf_distrib_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ια) (a : α) :
          a s.sup' hs f = s.sup' hs fun (i : ι) => a f i
          theorem Finset.sup'_inf_distrib_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ια) (a : α) :
          s.sup' hs f a = s.sup' hs fun (i : ι) => f i a
          theorem Finset.sup'_inf_sup' {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [DistribLattice α] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ια) (g : κα) :
          s.sup' hs f t.sup' ht g = (s ×ˢ t).sup' fun (i : ι × κ) => f i.1 g i.2
          theorem Finset.inf'_sup_distrib_left {α : Type u_2} {ι : Type u_5} [DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ια) (a : α) :
          a s.inf' hs f = s.inf' hs fun (i : ι) => a f i
          theorem Finset.inf'_sup_distrib_right {α : Type u_2} {ι : Type u_5} [DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ια) (a : α) :
          s.inf' hs f a = s.inf' hs fun (i : ι) => f i a
          theorem Finset.inf'_sup_inf' {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [DistribLattice α] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ια) (g : κα) :
          s.inf' hs f t.inf' ht g = (s ×ˢ t).inf' fun (i : ι × κ) => f i.1 g i.2
          @[simp]
          theorem Finset.le_sup'_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ια} {a : α} :
          a s.sup' H f bs, a f b
          @[simp]
          theorem Finset.lt_sup'_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ια} {a : α} :
          a < s.sup' H f bs, a < f b
          @[simp]
          theorem Finset.sup'_lt_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ια} {a : α} :
          s.sup' H f < a is, f i < a
          @[simp]
          theorem Finset.inf'_le_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ια} {a : α} :
          s.inf' H f a is, f i a
          @[simp]
          theorem Finset.inf'_lt_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ια} {a : α} :
          s.inf' H f < a is, f i < a
          @[simp]
          theorem Finset.lt_inf'_iff {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) {f : ια} {a : α} :
          a < s.inf' H f is, a < f i
          theorem Finset.exists_mem_eq_sup' {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) (f : ια) :
          is, s.sup' H f = f i
          theorem Finset.exists_mem_eq_inf' {α : Type u_2} {ι : Type u_5} [LinearOrder α] {s : Finset ι} (H : s.Nonempty) (f : ια) :
          is, s.inf' H f = f i
          theorem Finset.exists_mem_eq_sup {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderBot α] (s : Finset ι) (h : s.Nonempty) (f : ια) :
          is, s.sup f = f i
          theorem Finset.exists_mem_eq_inf {α : Type u_2} {ι : Type u_5} [LinearOrder α] [OrderTop α] (s : Finset ι) (h : s.Nonempty) (f : ια) :
          is, s.inf f = f i

          max and min of finite sets #

          def Finset.max {α : Type u_2} [LinearOrder α] (s : Finset α) :

          Let s be a finset in a linear order. Then s.max is the maximum of s if s is not empty, and otherwise. It belongs to WithBot α. If you want to get an element of α, see s.max'.

          Equations
          • s.max = s.sup WithBot.some
          Instances For
            theorem Finset.max_eq_sup_coe {α : Type u_2} [LinearOrder α] {s : Finset α} :
            s.max = s.sup WithBot.some
            theorem Finset.max_eq_sup_withBot {α : Type u_2} [LinearOrder α] (s : Finset α) :
            s.max = s.sup WithBot.some
            @[simp]
            theorem Finset.max_empty {α : Type u_2} [LinearOrder α] :
            .max =
            @[simp]
            theorem Finset.max_insert {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} :
            (insert a s).max = max (a) s.max
            @[simp]
            theorem Finset.max_singleton {α : Type u_2} [LinearOrder α] {a : α} :
            {a}.max = a
            theorem Finset.max_of_mem {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} (h : a s) :
            ∃ (b : α), s.max = b
            theorem Finset.max_of_nonempty {α : Type u_2} [LinearOrder α] {s : Finset α} (h : s.Nonempty) :
            ∃ (a : α), s.max = a
            theorem Finset.max_eq_bot {α : Type u_2} [LinearOrder α] {s : Finset α} :
            s.max = s =
            theorem Finset.mem_of_max {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} :
            s.max = aa s
            theorem Finset.le_max {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (as : a s) :
            a s.max
            theorem Finset.not_mem_of_max_lt_coe {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (h : s.max < a) :
            as
            theorem Finset.le_max_of_eq {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} {b : α} (h₁ : a s) (h₂ : s.max = b) :
            a b
            theorem Finset.not_mem_of_max_lt {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} {b : α} (h₁ : b < a) (h₂ : s.max = b) :
            as
            theorem Finset.max_mono {α : Type u_2} [LinearOrder α] {s : Finset α} {t : Finset α} (st : s t) :
            s.max t.max
            theorem Finset.max_le {α : Type u_2} [LinearOrder α] {M : WithBot α} {s : Finset α} (st : as, a M) :
            s.max M
            @[simp]
            theorem Finset.max_le_iff {α : Type u_2} [LinearOrder α] {m : WithBot α} {s : Finset α} :
            s.max m as, a m
            @[simp]
            theorem Finset.max_eq_top {α : Type u_2} [LinearOrder α] [OrderTop α] {s : Finset α} :
            s.max = s
            def Finset.min {α : Type u_2} [LinearOrder α] (s : Finset α) :

            Let s be a finset in a linear order. Then s.min is the minimum of s if s is not empty, and otherwise. It belongs to WithTop α. If you want to get an element of α, see s.min'.

            Equations
            • s.min = s.inf WithTop.some
            Instances For
              theorem Finset.min_eq_inf_withTop {α : Type u_2} [LinearOrder α] (s : Finset α) :
              s.min = s.inf WithTop.some
              @[simp]
              theorem Finset.min_empty {α : Type u_2} [LinearOrder α] :
              .min =
              @[simp]
              theorem Finset.min_insert {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} :
              (insert a s).min = min (a) s.min
              @[simp]
              theorem Finset.min_singleton {α : Type u_2} [LinearOrder α] {a : α} :
              {a}.min = a
              theorem Finset.min_of_mem {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} (h : a s) :
              ∃ (b : α), s.min = b
              theorem Finset.min_of_nonempty {α : Type u_2} [LinearOrder α] {s : Finset α} (h : s.Nonempty) :
              ∃ (a : α), s.min = a
              @[simp]
              theorem Finset.min_eq_top {α : Type u_2} [LinearOrder α] {s : Finset α} :
              s.min = s =
              theorem Finset.mem_of_min {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} :
              s.min = aa s
              theorem Finset.min_le {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (as : a s) :
              s.min a
              theorem Finset.not_mem_of_coe_lt_min {α : Type u_2} [LinearOrder α] {a : α} {s : Finset α} (h : a < s.min) :
              as
              theorem Finset.min_le_of_eq {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} {b : α} (h₁ : b s) (h₂ : s.min = a) :
              a b
              theorem Finset.not_mem_of_lt_min {α : Type u_2} [LinearOrder α] {s : Finset α} {a : α} {b : α} (h₁ : a < b) (h₂ : s.min = b) :
              as
              theorem Finset.min_mono {α : Type u_2} [LinearOrder α] {s : Finset α} {t : Finset α} (st : s t) :
              t.min s.min
              theorem Finset.le_min {α : Type u_2} [LinearOrder α] {m : WithTop α} {s : Finset α} (st : as, m a) :
              m s.min
              @[simp]
              theorem Finset.le_min_iff {α : Type u_2} [LinearOrder α] {m : WithTop α} {s : Finset α} :
              m s.min as, m a
              @[simp]
              theorem Finset.min_eq_bot {α : Type u_2} [LinearOrder α] [OrderBot α] {s : Finset α} :
              s.min = s
              def Finset.min' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) :
              α

              Given a nonempty finset s in a linear order α, then s.min' h is its minimum, as an element of α, where h is a proof of nonemptiness. Without this assumption, use instead s.min, taking values in WithTop α.

              Equations
              • s.min' H = s.inf' H id
              Instances For
                def Finset.max' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) :
                α

                Given a nonempty finset s in a linear order α, then s.max' h is its maximum, as an element of α, where h is a proof of nonemptiness. Without this assumption, use instead s.max, taking values in WithBot α.

                Equations
                • s.max' H = s.sup' H id
                Instances For
                  theorem Finset.min'_mem {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) :
                  s.min' H s
                  theorem Finset.min'_le {α : Type u_2} [LinearOrder α] (s : Finset α) (x : α) (H2 : x s) :
                  s.min' x
                  theorem Finset.le_min' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) (x : α) (H2 : ys, x y) :
                  x s.min' H
                  theorem Finset.isLeast_min' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) :
                  IsLeast (s) (s.min' H)
                  @[simp]
                  theorem Finset.le_min'_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} :
                  x s.min' H ys, x y
                  @[simp]
                  theorem Finset.min'_singleton {α : Type u_2} [LinearOrder α] (a : α) :
                  {a}.min' = a

                  {a}.min' _ is a.

                  theorem Finset.max'_mem {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) :
                  s.max' H s
                  theorem Finset.le_max' {α : Type u_2} [LinearOrder α] (s : Finset α) (x : α) (H2 : x s) :
                  x s.max'
                  theorem Finset.max'_le {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) (x : α) (H2 : ys, y x) :
                  s.max' H x
                  theorem Finset.isGreatest_max' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) :
                  IsGreatest (s) (s.max' H)
                  @[simp]
                  theorem Finset.max'_le_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} :
                  s.max' H x ys, y x
                  @[simp]
                  theorem Finset.max'_lt_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} :
                  s.max' H < x ys, y < x
                  @[simp]
                  theorem Finset.lt_min'_iff {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α} :
                  x < s.min' H ys, x < y
                  theorem Finset.max'_eq_sup' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) :
                  s.max' H = s.sup' H id
                  theorem Finset.min'_eq_inf' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) :
                  s.min' H = s.inf' H id
                  @[simp]
                  theorem Finset.max'_singleton {α : Type u_2} [LinearOrder α] (a : α) :
                  {a}.max' = a

                  {a}.max' _ is a.

                  theorem Finset.min'_lt_max' {α : Type u_2} [LinearOrder α] (s : Finset α) {i : α} {j : α} (H1 : i s) (H2 : j s) (H3 : i j) :
                  s.min' < s.max'
                  theorem Finset.min'_lt_max'_of_card {α : Type u_2} [LinearOrder α] (s : Finset α) (h₂ : 1 < s.card) :
                  s.min' < s.max'

                  If there's more than 1 element, the min' is less than the max'. An alternate version of min'_lt_max' which is sometimes more convenient.

                  theorem Finset.map_ofDual_min {α : Type u_2} [LinearOrder α] (s : Finset αᵒᵈ) :
                  WithTop.map (OrderDual.ofDual) s.min = (Finset.image (OrderDual.ofDual) s).max
                  theorem Finset.map_ofDual_max {α : Type u_2} [LinearOrder α] (s : Finset αᵒᵈ) :
                  WithBot.map (OrderDual.ofDual) s.max = (Finset.image (OrderDual.ofDual) s).min
                  theorem Finset.map_toDual_min {α : Type u_2} [LinearOrder α] (s : Finset α) :
                  WithTop.map (OrderDual.toDual) s.min = (Finset.image (OrderDual.toDual) s).max
                  theorem Finset.map_toDual_max {α : Type u_2} [LinearOrder α] (s : Finset α) :
                  WithBot.map (OrderDual.toDual) s.max = (Finset.image (OrderDual.toDual) s).min
                  theorem Finset.ofDual_min' {α : Type u_2} [LinearOrder α] {s : Finset αᵒᵈ} (hs : s.Nonempty) :
                  OrderDual.ofDual (s.min' hs) = (Finset.image (OrderDual.ofDual) s).max'
                  theorem Finset.ofDual_max' {α : Type u_2} [LinearOrder α] {s : Finset αᵒᵈ} (hs : s.Nonempty) :
                  OrderDual.ofDual (s.max' hs) = (Finset.image (OrderDual.ofDual) s).min'
                  theorem Finset.toDual_min' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) :
                  OrderDual.toDual (s.min' hs) = (Finset.image (OrderDual.toDual) s).max'
                  theorem Finset.toDual_max' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) :
                  OrderDual.toDual (s.max' hs) = (Finset.image (OrderDual.toDual) s).min'
                  theorem Finset.max'_subset {α : Type u_2} [LinearOrder α] {s : Finset α} {t : Finset α} (H : s.Nonempty) (hst : s t) :
                  s.max' H t.max'
                  theorem Finset.min'_subset {α : Type u_2} [LinearOrder α] {s : Finset α} {t : Finset α} (H : s.Nonempty) (hst : s t) :
                  t.min' s.min' H
                  theorem Finset.max'_insert {α : Type u_2} [LinearOrder α] (a : α) (s : Finset α) (H : s.Nonempty) :
                  (insert a s).max' = max (s.max' H) a
                  theorem Finset.min'_insert {α : Type u_2} [LinearOrder α] (a : α) (s : Finset α) (H : s.Nonempty) :
                  (insert a s).min' = min (s.min' H) a
                  theorem Finset.lt_max'_of_mem_erase_max' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) [DecidableEq α] {a : α} (ha : a s.erase (s.max' H)) :
                  a < s.max' H
                  theorem Finset.min'_lt_of_mem_erase_min' {α : Type u_2} [LinearOrder α] (s : Finset α) (H : s.Nonempty) [DecidableEq α] {a : α} (ha : a s.erase (s.min' H)) :
                  s.min' H < a
                  @[simp]
                  theorem Finset.max'_image {α : Type u_2} {β : Type u_3} [LinearOrder α] [LinearOrder β] {f : αβ} (hf : Monotone f) (s : Finset α) (h : (Finset.image f s).Nonempty) :
                  (Finset.image f s).max' h = f (s.max' )

                  To rewrite from right to left, use Monotone.map_finset_max'.

                  theorem Monotone.map_finset_max' {α : Type u_2} {β : Type u_3} [LinearOrder α] [LinearOrder β] {f : αβ} (hf : Monotone f) {s : Finset α} (h : s.Nonempty) :
                  f (s.max' h) = (Finset.image f s).max'

                  A version of Finset.max'_image with LHS and RHS reversed. Also, this version assumes that s is nonempty, not its image.

                  @[simp]
                  theorem Finset.min'_image {α : Type u_2} {β : Type u_3} [LinearOrder α] [LinearOrder β] {f : αβ} (hf : Monotone f) (s : Finset α) (h : (Finset.image f s).Nonempty) :
                  (Finset.image f s).min' h = f (s.min' )

                  To rewrite from right to left, use Monotone.map_finset_min'.

                  theorem Monotone.map_finset_min' {α : Type u_2} {β : Type u_3} [LinearOrder α] [LinearOrder β] {f : αβ} (hf : Monotone f) {s : Finset α} (h : s.Nonempty) :
                  f (s.min' h) = (Finset.image f s).min'

                  A version of Finset.min'_image with LHS and RHS reversed. Also, this version assumes that s is nonempty, not its image.

                  theorem Finset.coe_max' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) :
                  (s.max' hs) = s.max
                  theorem Finset.coe_min' {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) :
                  (s.min' hs) = s.min
                  theorem Finset.max_mem_image_coe {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) :
                  s.max Finset.image WithBot.some s
                  theorem Finset.min_mem_image_coe {α : Type u_2} [LinearOrder α] {s : Finset α} (hs : s.Nonempty) :
                  s.min Finset.image WithTop.some s
                  theorem Finset.max_mem_insert_bot_image_coe {α : Type u_2} [LinearOrder α] (s : Finset α) :
                  s.max insert (Finset.image WithBot.some s)
                  theorem Finset.min_mem_insert_top_image_coe {α : Type u_2} [LinearOrder α] (s : Finset α) :
                  s.min insert (Finset.image WithTop.some s)
                  theorem Finset.max'_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} (s0 : (s.erase x).Nonempty) :
                  (s.erase x).max' s0 x
                  theorem Finset.min'_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} (s0 : (s.erase x).Nonempty) :
                  (s.erase x).min' s0 x
                  theorem Finset.max_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} :
                  (s.erase x).max x
                  theorem Finset.min_erase_ne_self {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} :
                  (s.erase x).min x
                  theorem Finset.exists_next_right {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} (h : ys, x < y) :
                  ys, x < y zs, x < zy z
                  theorem Finset.exists_next_left {α : Type u_2} [LinearOrder α] {x : α} {s : Finset α} (h : ys, y < x) :
                  ys, y < x zs, z < xz y
                  theorem Finset.card_le_of_interleaved {α : Type u_2} [LinearOrder α] {s : Finset α} {t : Finset α} (h : xs, ys, x < y(zs, zSet.Ioo x y)zt, x < z z < y) :
                  s.card t.card + 1

                  If finsets s and t are interleaved, then Finset.card s ≤ Finset.card t + 1.

                  theorem Finset.card_le_diff_of_interleaved {α : Type u_2} [LinearOrder α] {s : Finset α} {t : Finset α} (h : xs, ys, x < y(zs, zSet.Ioo x y)zt, x < z z < y) :
                  s.card (t \ s).card + 1

                  If finsets s and t are interleaved, then Finset.card s ≤ Finset.card (t \ s) + 1.

                  theorem Finset.induction_on_max {α : Type u_2} [LinearOrder α] [DecidableEq α] {p : Finset αProp} (s : Finset α) (h0 : p ) (step : ∀ (a : α) (s : Finset α), (xs, x < a)p sp (insert a s)) :
                  p s

                  Induction principle for Finsets in a linearly ordered type: a predicate is true on all s : Finset α provided that:

                  • it is true on the empty Finset,
                  • for every s : Finset α and an element a strictly greater than all elements of s, p s implies p (insert a s).
                  theorem Finset.induction_on_min {α : Type u_2} [LinearOrder α] [DecidableEq α] {p : Finset αProp} (s : Finset α) (h0 : p ) (step : ∀ (a : α) (s : Finset α), (xs, a < x)p sp (insert a s)) :
                  p s

                  Induction principle for Finsets in a linearly ordered type: a predicate is true on all s : Finset α provided that:

                  • it is true on the empty Finset,
                  • for every s : Finset α and an element a strictly less than all elements of s, p s implies p (insert a s).
                  theorem Finset.induction_on_max_value {α : Type u_2} {ι : Type u_5} [LinearOrder α] [DecidableEq ι] (f : ια) {p : Finset ιProp} (s : Finset ι) (h0 : p ) (step : ∀ (a : ι) (s : Finset ι), as(xs, f x f a)p sp (insert a s)) :
                  p s

                  Induction principle for Finsets in any type from which a given function f maps to a linearly ordered type : a predicate is true on all s : Finset α provided that:

                  • it is true on the empty Finset,
                  • for every s : Finset α and an element a such that for elements of s denoted by x we have f x ≤ f a, p s implies p (insert a s).
                  theorem Finset.induction_on_min_value {α : Type u_2} {ι : Type u_5} [LinearOrder α] [DecidableEq ι] (f : ια) {p : Finset ιProp} (s : Finset ι) (h0 : p ) (step : ∀ (a : ι) (s : Finset ι), as(xs, f a f x)p sp (insert a s)) :
                  p s

                  Induction principle for Finsets in any type from which a given function f maps to a linearly ordered type : a predicate is true on all s : Finset α provided that:

                  • it is true on the empty Finset,
                  • for every s : Finset α and an element a such that for elements of s denoted by x we have f a ≤ f x, p s implies p (insert a s).
                  theorem Finset.exists_max_image {α : Type u_2} {β : Type u_3} [LinearOrder α] (s : Finset β) (f : βα) (h : s.Nonempty) :
                  xs, x's, f x' f x
                  theorem Finset.exists_min_image {α : Type u_2} {β : Type u_3} [LinearOrder α] (s : Finset β) (f : βα) (h : s.Nonempty) :
                  xs, x's, f x f x'
                  theorem Finset.isGLB_iff_isLeast {α : Type u_2} [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) :
                  IsGLB (s) i IsLeast (s) i
                  theorem Finset.isLUB_iff_isGreatest {α : Type u_2} [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) :
                  IsLUB (s) i IsGreatest (s) i
                  theorem Finset.isGLB_mem {α : Type u_2} [LinearOrder α] {i : α} (s : Finset α) (his : IsGLB (s) i) (hs : s.Nonempty) :
                  i s
                  theorem Finset.isLUB_mem {α : Type u_2} [LinearOrder α] {i : α} (s : Finset α) (his : IsLUB (s) i) (hs : s.Nonempty) :
                  i s
                  theorem Multiset.map_finset_sup {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] [DecidableEq β] (s : Finset γ) (f : γMultiset β) (g : βα) (hg : Function.Injective g) :
                  Multiset.map g (s.sup f) = s.sup (Multiset.map g f)
                  theorem Multiset.count_finset_sup {α : Type u_2} {β : Type u_3} [DecidableEq β] (s : Finset α) (f : αMultiset β) (b : β) :
                  Multiset.count b (s.sup f) = s.sup fun (a : α) => Multiset.count b (f a)
                  theorem Multiset.mem_sup {α : Type u_7} {β : Type u_8} [DecidableEq β] {s : Finset α} {f : αMultiset β} {x : β} :
                  x s.sup f vs, x f v
                  theorem Finset.mem_sup {α : Type u_7} {β : Type u_8} [DecidableEq β] {s : Finset α} {f : αFinset β} {x : β} :
                  x s.sup f vs, x f v
                  theorem Finset.sup_eq_biUnion {α : Type u_7} {β : Type u_8} [DecidableEq β] (s : Finset α) (t : αFinset β) :
                  s.sup t = s.biUnion t
                  @[simp]
                  theorem Finset.sup_singleton'' {α : Type u_2} {β : Type u_3} [DecidableEq α] (s : Finset β) (f : βα) :
                  (s.sup fun (b : β) => {f b}) = Finset.image f s
                  @[simp]
                  theorem Finset.sup_singleton' {α : Type u_2} [DecidableEq α] (s : Finset α) :
                  s.sup singleton = s
                  theorem iSup_eq_iSup_finset {α : Type u_2} {ι : Type u_5} [CompleteLattice α] (s : ια) :
                  ⨆ (i : ι), s i = ⨆ (t : Finset ι), it, s i

                  Supremum of s i, i : ι, is equal to the supremum over t : Finset ι of suprema ⨆ i ∈ t, s i. This version assumes ι is a Type*. See iSup_eq_iSup_finset' for a version that works for ι : Sort*.

                  theorem iSup_eq_iSup_finset' {α : Type u_2} {ι' : Sort u_7} [CompleteLattice α] (s : ι'α) :
                  ⨆ (i : ι'), s i = ⨆ (t : Finset (PLift ι')), it, s i.down

                  Supremum of s i, i : ι, is equal to the supremum over t : Finset ι of suprema ⨆ i ∈ t, s i. This version works for ι : Sort*. See iSup_eq_iSup_finset for a version that assumes ι : Type* but has no PLifts.

                  theorem iInf_eq_iInf_finset {α : Type u_2} {ι : Type u_5} [CompleteLattice α] (s : ια) :
                  ⨅ (i : ι), s i = ⨅ (t : Finset ι), it, s i

                  Infimum of s i, i : ι, is equal to the infimum over t : Finset ι of infima ⨅ i ∈ t, s i. This version assumes ι is a Type*. See iInf_eq_iInf_finset' for a version that works for ι : Sort*.

                  theorem iInf_eq_iInf_finset' {α : Type u_2} {ι' : Sort u_7} [CompleteLattice α] (s : ι'α) :
                  ⨅ (i : ι'), s i = ⨅ (t : Finset (PLift ι')), it, s i.down

                  Infimum of s i, i : ι, is equal to the infimum over t : Finset ι of infima ⨅ i ∈ t, s i. This version works for ι : Sort*. See iInf_eq_iInf_finset for a version that assumes ι : Type* but has no PLifts.

                  theorem Set.iUnion_eq_iUnion_finset {α : Type u_2} {ι : Type u_5} (s : ιSet α) :
                  ⋃ (i : ι), s i = ⋃ (t : Finset ι), it, s i

                  Union of an indexed family of sets s : ι → Set α is equal to the union of the unions of finite subfamilies. This version assumes ι : Type*. See also iUnion_eq_iUnion_finset' for a version that works for ι : Sort*.

                  theorem Set.iUnion_eq_iUnion_finset' {α : Type u_2} {ι' : Sort u_7} (s : ι'Set α) :
                  ⋃ (i : ι'), s i = ⋃ (t : Finset (PLift ι')), it, s i.down

                  Union of an indexed family of sets s : ι → Set α is equal to the union of the unions of finite subfamilies. This version works for ι : Sort*. See also iUnion_eq_iUnion_finset for a version that assumes ι : Type* but avoids PLifts in the right hand side.

                  theorem Set.iInter_eq_iInter_finset {α : Type u_2} {ι : Type u_5} (s : ιSet α) :
                  ⋂ (i : ι), s i = ⋂ (t : Finset ι), it, s i

                  Intersection of an indexed family of sets s : ι → Set α is equal to the intersection of the intersections of finite subfamilies. This version assumes ι : Type*. See also iInter_eq_iInter_finset' for a version that works for ι : Sort*.

                  theorem Set.iInter_eq_iInter_finset' {α : Type u_2} {ι' : Sort u_7} (s : ι'Set α) :
                  ⋂ (i : ι'), s i = ⋂ (t : Finset (PLift ι')), it, s i.down

                  Intersection of an indexed family of sets s : ι → Set α is equal to the intersection of the intersections of finite subfamilies. This version works for ι : Sort*. See also iInter_eq_iInter_finset for a version that assumes ι : Type* but avoids PLifts in the right hand side.

                  theorem Finset.mem_maximals_iff_forall_insert {α : Type u_2} [DecidableEq α] {P : Finset αProp} {s : Finset α} (hP : ∀ ⦃s t : Finset α⦄, P ts tP s) :
                  s maximals (fun (x x_1 : Finset α) => x x_1) {t : Finset α | P t} P s xs, ¬P (insert x s)
                  theorem Finset.mem_minimals_iff_forall_erase {α : Type u_2} [DecidableEq α] {P : Finset αProp} {s : Finset α} (hP : ∀ ⦃s t : Finset α⦄, P ss tP t) :
                  s minimals (fun (x x_1 : Finset α) => x x_1) {t : Finset α | P t} P s xs, ¬P (s.erase x)

                  Interaction with big lattice/set operations #

                  theorem Finset.iSup_coe {α : Type u_2} {β : Type u_3} [SupSet β] (f : αβ) (s : Finset α) :
                  xs, f x = xs, f x
                  theorem Finset.iInf_coe {α : Type u_2} {β : Type u_3} [InfSet β] (f : αβ) (s : Finset α) :
                  xs, f x = xs, f x
                  theorem Finset.iSup_singleton {α : Type u_2} {β : Type u_3} [CompleteLattice β] (a : α) (s : αβ) :
                  x{a}, s x = s a
                  theorem Finset.iInf_singleton {α : Type u_2} {β : Type u_3} [CompleteLattice β] (a : α) (s : αβ) :
                  x{a}, s x = s a
                  theorem Finset.iSup_option_toFinset {α : Type u_2} {β : Type u_3} [CompleteLattice β] (o : Option α) (f : αβ) :
                  xo.toFinset, f x = xo, f x
                  theorem Finset.iInf_option_toFinset {α : Type u_2} {β : Type u_3} [CompleteLattice β] (o : Option α) (f : αβ) :
                  xo.toFinset, f x = xo, f x
                  theorem Finset.iSup_union {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] {f : αβ} {s : Finset α} {t : Finset α} :
                  xs t, f x = (xs, f x) xt, f x
                  theorem Finset.iInf_union {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] {f : αβ} {s : Finset α} {t : Finset α} :
                  xs t, f x = (xs, f x) xt, f x
                  theorem Finset.iSup_insert {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] (a : α) (s : Finset α) (t : αβ) :
                  xinsert a s, t x = t a xs, t x
                  theorem Finset.iInf_insert {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] (a : α) (s : Finset α) (t : αβ) :
                  xinsert a s, t x = t a xs, t x
                  theorem Finset.iSup_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice β] [DecidableEq α] {f : γα} {g : αβ} {s : Finset γ} :
                  xFinset.image f s, g x = ys, g (f y)
                  theorem Finset.iInf_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice β] [DecidableEq α] {f : γα} {g : αβ} {s : Finset γ} :
                  xFinset.image f s, g x = ys, g (f y)
                  theorem Finset.iSup_insert_update {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] {x : α} {t : Finset α} (f : αβ) {s : β} (hx : xt) :
                  iinsert x t, Function.update f x s i = s it, f i
                  theorem Finset.iInf_insert_update {α : Type u_2} {β : Type u_3} [CompleteLattice β] [DecidableEq α] {x : α} {t : Finset α} (f : αβ) {s : β} (hx : xt) :
                  iinsert x t, Function.update f x s i = s it, f i
                  theorem Finset.iSup_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice β] [DecidableEq α] (s : Finset γ) (t : γFinset α) (f : αβ) :
                  ys.biUnion t, f y = xs, yt x, f y
                  theorem Finset.iInf_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CompleteLattice β] [DecidableEq α] (s : Finset γ) (t : γFinset α) (f : αβ) :
                  ys.biUnion t, f y = xs, yt x, f y
                  theorem Finset.set_biUnion_coe {α : Type u_2} {β : Type u_3} (s : Finset α) (t : αSet β) :
                  xs, t x = xs, t x
                  theorem Finset.set_biInter_coe {α : Type u_2} {β : Type u_3} (s : Finset α) (t : αSet β) :
                  xs, t x = xs, t x
                  theorem Finset.set_biUnion_singleton {α : Type u_2} {β : Type u_3} (a : α) (s : αSet β) :
                  x{a}, s x = s a
                  theorem Finset.set_biInter_singleton {α : Type u_2} {β : Type u_3} (a : α) (s : αSet β) :
                  x{a}, s x = s a
                  @[simp]
                  theorem Finset.set_biUnion_preimage_singleton {α : Type u_2} {β : Type u_3} (f : αβ) (s : Finset β) :
                  ys, f ⁻¹' {y} = f ⁻¹' s
                  theorem Finset.set_biUnion_option_toFinset {α : Type u_2} {β : Type u_3} (o : Option α) (f : αSet β) :
                  xo.toFinset, f x = xo, f x
                  theorem Finset.set_biInter_option_toFinset {α : Type u_2} {β : Type u_3} (o : Option α) (f : αSet β) :
                  xo.toFinset, f x = xo, f x
                  theorem Finset.subset_set_biUnion_of_mem {α : Type u_2} {β : Type u_3} {s : Finset α} {f : αSet β} {x : α} (h : x s) :
                  f x ys, f y
                  theorem Finset.set_biUnion_union {α : Type u_2} {β : Type u_3} [DecidableEq α] (s : Finset α) (t : Finset α) (u : αSet β) :
                  xs t, u x = (xs, u x) xt, u x
                  theorem Finset.set_biInter_inter {α : Type u_2} {β : Type u_3} [DecidableEq α] (s : Finset α) (t : Finset α) (u : αSet β) :
                  xs t, u x = (xs, u x) xt, u x
                  theorem Finset.set_biUnion_insert {α : Type u_2} {β : Type u_3} [DecidableEq α] (a : α) (s : Finset α) (t : αSet β) :
                  xinsert a s, t x = t a xs, t x
                  theorem Finset.set_biInter_insert {α : Type u_2} {β : Type u_3} [DecidableEq α] (a : α) (s : Finset α) (t : αSet β) :
                  xinsert a s, t x = t a xs, t x
                  theorem Finset.set_biUnion_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] {f : γα} {g : αSet β} {s : Finset γ} :
                  xFinset.image f s, g x = ys, g (f y)
                  theorem Finset.set_biInter_finset_image {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] {f : γα} {g : αSet β} {s : Finset γ} :
                  xFinset.image f s, g x = ys, g (f y)
                  theorem Finset.set_biUnion_insert_update {α : Type u_2} {β : Type u_3} [DecidableEq α] {x : α} {t : Finset α} (f : αSet β) {s : Set β} (hx : xt) :
                  iinsert x t, Function.update f x s i = s it, f i
                  theorem Finset.set_biInter_insert_update {α : Type u_2} {β : Type u_3} [DecidableEq α] {x : α} {t : Finset α} (f : αSet β) {s : Set β} (hx : xt) :
                  iinsert x t, Function.update f x s i = s it, f i
                  theorem Finset.set_biUnion_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] (s : Finset γ) (t : γFinset α) (f : αSet β) :
                  ys.biUnion t, f y = xs, yt x, f y
                  theorem Finset.set_biInter_biUnion {α : Type u_2} {β : Type u_3} {γ : Type u_4} [DecidableEq α] (s : Finset γ) (t : γFinset α) (f : αSet β) :
                  ys.biUnion t, f y = xs, yt x, f y