Documentation

Mathlib.Order.CompleteLattice

Theory of complete lattices #

Main definitions #

Naming conventions #

In lemma names,

Notation #

@[simp]
theorem iSup_ulift {α : Type u_1} {ι : Type u_8} [SupSet α] (f : ULift.{u_9, u_8} ια) :
⨆ (i : ULift.{u_9, u_8} ι), f i = ⨆ (i : ι), f { down := i }
@[simp]
theorem iInf_ulift {α : Type u_1} {ι : Type u_8} [InfSet α] (f : ULift.{u_9, u_8} ια) :
⨅ (i : ULift.{u_9, u_8} ι), f i = ⨅ (i : ι), f { down := i }
instance OrderDual.supSet (α : Type u_8) [InfSet α] :
Equations
instance OrderDual.infSet (α : Type u_8) [SupSet α] :
Equations
class CompleteSemilatticeSup (α : Type u_8) extends PartialOrder , SupSet :
Type u_8

Note that we rarely use CompleteSemilatticeSup (in fact, any such object is always a CompleteLattice, so it's usually best to start there).

Nevertheless it is sometimes a useful intermediate step in constructions.

  • le : ααProp
  • lt : ααProp
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • sSup : Set αα
  • le_sSup : ∀ (s : Set α), as, a sSup s

    Any element of a set is less than the set supremum.

  • sSup_le : ∀ (s : Set α) (a : α), (∀ bs, b a)sSup s a

    Any upper bound is more than the set supremum.

Instances
    theorem CompleteSemilatticeSup.le_sSup {α : Type u_8} [self : CompleteSemilatticeSup α] (s : Set α) (a : α) :
    a sa sSup s

    Any element of a set is less than the set supremum.

    theorem CompleteSemilatticeSup.sSup_le {α : Type u_8} [self : CompleteSemilatticeSup α] (s : Set α) (a : α) :
    (∀ bs, b a)sSup s a

    Any upper bound is more than the set supremum.

    theorem le_sSup {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} :
    a sa sSup s
    theorem sSup_le {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} :
    (∀ bs, b a)sSup s a
    theorem isLUB_sSup {α : Type u_1} [CompleteSemilatticeSup α] (s : Set α) :
    IsLUB s (sSup s)
    theorem isLUB_iff_sSup_eq {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} :
    IsLUB s a sSup s = a
    theorem IsLUB.sSup_eq {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} :
    IsLUB s asSup s = a

    Alias of the forward direction of isLUB_iff_sSup_eq.

    theorem le_sSup_of_le {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} {b : α} (hb : b s) (h : a b) :
    a sSup s
    theorem sSup_le_sSup {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {t : Set α} (h : s t) :
    @[simp]
    theorem sSup_le_iff {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} :
    sSup s a bs, b a
    theorem le_sSup_iff {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} :
    a sSup s bupperBounds s, a b
    theorem le_iSup_iff {α : Type u_1} {ι : Sort u_4} [CompleteSemilatticeSup α] {a : α} {s : ια} :
    a iSup s ∀ (b : α), (∀ (i : ι), s i b)a b
    theorem sSup_le_sSup_of_forall_exists_le {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {t : Set α} (h : xs, yt, x y) :
    theorem sSup_singleton {α : Type u_1} [CompleteSemilatticeSup α] {a : α} :
    sSup {a} = a
    class CompleteSemilatticeInf (α : Type u_8) extends PartialOrder , InfSet :
    Type u_8

    Note that we rarely use CompleteSemilatticeInf (in fact, any such object is always a CompleteLattice, so it's usually best to start there).

    Nevertheless it is sometimes a useful intermediate step in constructions.

    • le : ααProp
    • lt : ααProp
    • le_refl : ∀ (a : α), a a
    • le_trans : ∀ (a b c : α), a bb ca c
    • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
    • le_antisymm : ∀ (a b : α), a bb aa = b
    • sInf : Set αα
    • sInf_le : ∀ (s : Set α), as, sInf s a

      Any element of a set is more than the set infimum.

    • le_sInf : ∀ (s : Set α) (a : α), (∀ bs, a b)a sInf s

      Any lower bound is less than the set infimum.

    Instances
      theorem CompleteSemilatticeInf.sInf_le {α : Type u_8} [self : CompleteSemilatticeInf α] (s : Set α) (a : α) :
      a ssInf s a

      Any element of a set is more than the set infimum.

      theorem CompleteSemilatticeInf.le_sInf {α : Type u_8} [self : CompleteSemilatticeInf α] (s : Set α) (a : α) :
      (∀ bs, a b)a sInf s

      Any lower bound is less than the set infimum.

      theorem sInf_le {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} :
      a ssInf s a
      theorem le_sInf {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} :
      (∀ bs, a b)a sInf s
      theorem isGLB_sInf {α : Type u_1} [CompleteSemilatticeInf α] (s : Set α) :
      IsGLB s (sInf s)
      theorem isGLB_iff_sInf_eq {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} :
      IsGLB s a sInf s = a
      theorem IsGLB.sInf_eq {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} :
      IsGLB s asInf s = a

      Alias of the forward direction of isGLB_iff_sInf_eq.

      theorem sInf_le_of_le {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} {b : α} (hb : b s) (h : b a) :
      sInf s a
      theorem sInf_le_sInf {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {t : Set α} (h : s t) :
      @[simp]
      theorem le_sInf_iff {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} :
      a sInf s bs, a b
      theorem sInf_le_iff {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} :
      sInf s a blowerBounds s, b a
      theorem iInf_le_iff {α : Type u_1} {ι : Sort u_4} [CompleteSemilatticeInf α] {a : α} {s : ια} :
      iInf s a ∀ (b : α), (∀ (i : ι), b s i)b a
      theorem sInf_le_sInf_of_forall_exists_le {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {t : Set α} (h : xs, yt, y x) :
      theorem sInf_singleton {α : Type u_1} [CompleteSemilatticeInf α] {a : α} :
      sInf {a} = a
      class CompleteLattice (α : Type u_8) extends Lattice , SupSet , InfSet , Top , Bot :
      Type u_8

      A complete lattice is a bounded lattice which has suprema and infima for every subset.

      • sup : ααα
      • le : ααProp
      • lt : ααProp
      • le_refl : ∀ (a : α), a a
      • le_trans : ∀ (a b c : α), a bb ca c
      • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
      • le_antisymm : ∀ (a b : α), a bb aa = b
      • le_sup_left : ∀ (a b : α), a a b
      • le_sup_right : ∀ (a b : α), b a b
      • sup_le : ∀ (a b c : α), a cb ca b c
      • inf : ααα
      • inf_le_left : ∀ (a b : α), a b a
      • inf_le_right : ∀ (a b : α), a b b
      • le_inf : ∀ (a b c : α), a ba ca b c
      • sSup : Set αα
      • le_sSup : ∀ (s : Set α), as, a sSup s

        Any element of a set is less than the set supremum.

      • sSup_le : ∀ (s : Set α) (a : α), (∀ bs, b a)sSup s a

        Any upper bound is more than the set supremum.

      • sInf : Set αα
      • sInf_le : ∀ (s : Set α), as, sInf s a

        Any element of a set is more than the set infimum.

      • le_sInf : ∀ (s : Set α) (a : α), (∀ bs, a b)a sInf s

        Any lower bound is less than the set infimum.

      • top : α
      • bot : α
      • le_top : ∀ (x : α), x

        Any element is less than the top one.

      • bot_le : ∀ (x : α), x

        Any element is more than the bottom one.

      Instances
        theorem CompleteLattice.le_top {α : Type u_8} [self : CompleteLattice α] (x : α) :

        Any element is less than the top one.

        theorem CompleteLattice.bot_le {α : Type u_8} [self : CompleteLattice α] (x : α) :

        Any element is more than the bottom one.

        @[instance 100]
        Equations
        • CompleteLattice.toBoundedOrder = BoundedOrder.mk
        def completeLatticeOfInf (α : Type u_8) [H1 : PartialOrder α] [H2 : InfSet α] (isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)) :

        Create a CompleteLattice from a PartialOrder and InfSet that returns the greatest lower bound of a set. Usually this constructor provides poor definitional equalities. If other fields are known explicitly, they should be provided; for example, if inf is known explicitly, construct the CompleteLattice instance as

        instance : CompleteLattice my_T where
          inf := better_inf
          le_inf := ...
          inf_le_right := ...
          inf_le_left := ...
          -- don't care to fix sup, sSup, bot, top
          __ := completeLatticeOfInf my_T _
        
        Equations
        Instances For

          Any CompleteSemilatticeInf is in fact a CompleteLattice.

          Note that this construction has bad definitional properties: see the doc-string on completeLatticeOfInf.

          Equations
          Instances For
            def completeLatticeOfSup (α : Type u_8) [H1 : PartialOrder α] [H2 : SupSet α] (isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)) :

            Create a CompleteLattice from a PartialOrder and SupSet that returns the least upper bound of a set. Usually this constructor provides poor definitional equalities. If other fields are known explicitly, they should be provided; for example, if inf is known explicitly, construct the CompleteLattice instance as

            instance : CompleteLattice my_T where
              inf := better_inf
              le_inf := ...
              inf_le_right := ...
              inf_le_left := ...
              -- don't care to fix sup, sInf, bot, top
              __ := completeLatticeOfSup my_T _
            
            Equations
            Instances For

              Any CompleteSemilatticeSup is in fact a CompleteLattice.

              Note that this construction has bad definitional properties: see the doc-string on completeLatticeOfSup.

              Equations
              Instances For
                class CompleteLinearOrder (α : Type u_8) extends CompleteLattice , HImp , HasCompl , SDiff , HNot :
                Type u_8

                A complete linear order is a linear order whose lattice structure is complete.

                • sup : ααα
                • le : ααProp
                • lt : ααProp
                • le_refl : ∀ (a : α), a a
                • le_trans : ∀ (a b c : α), a bb ca c
                • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
                • le_antisymm : ∀ (a b : α), a bb aa = b
                • le_sup_left : ∀ (a b : α), a a b
                • le_sup_right : ∀ (a b : α), b a b
                • sup_le : ∀ (a b c : α), a cb ca b c
                • inf : ααα
                • inf_le_left : ∀ (a b : α), a b a
                • inf_le_right : ∀ (a b : α), a b b
                • le_inf : ∀ (a b c : α), a ba ca b c
                • sSup : Set αα
                • le_sSup : ∀ (s : Set α), as, a sSup s
                • sSup_le : ∀ (s : Set α) (a : α), (∀ bs, b a)sSup s a
                • sInf : Set αα
                • sInf_le : ∀ (s : Set α), as, sInf s a
                • le_sInf : ∀ (s : Set α) (a : α), (∀ bs, a b)a sInf s
                • top : α
                • bot : α
                • le_top : ∀ (x : α), x
                • bot_le : ∀ (x : α), x
                • himp : ααα
                • le_himp_iff : ∀ (a b c : α), a b c a b c

                  (a ⇨ ·) is right adjoint to (a ⊓ ·)

                • compl : αα
                • himp_bot : ∀ (a : α), a = a

                  aᶜ is defined as a ⇨ ⊥

                • sdiff : ααα
                • hnot : αα
                • sdiff_le_iff : ∀ (a b c : α), a \ b c a b c

                  (· \ a) is right adjoint to (· ⊔ a)

                • top_sdiff : ∀ (a : α), \ a = a

                  ⊤ \ a is ¬a

                • le_total : ∀ (a b : α), a b b a

                  A linear order is total.

                • decidableLE : DecidableRel fun (x1 x2 : α) => x1 x2

                  In a linearly ordered type, we assume the order relations are all decidable.

                • decidableEq : DecidableEq α

                  In a linearly ordered type, we assume the order relations are all decidable.

                • decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2

                  In a linearly ordered type, we assume the order relations are all decidable.

                Instances
                  theorem CompleteLinearOrder.le_total {α : Type u_8} [self : CompleteLinearOrder α] (a : α) (b : α) :
                  a b b a

                  A linear order is total.

                  Equations
                  • CompleteLinearOrder.toLinearOrder = LinearOrder.mk CompleteLinearOrder.decidableLE CompleteLinearOrder.decidableEq CompleteLinearOrder.decidableLT
                  Equations
                  Equations
                  • OrderDual.instCompleteLinearOrder = CompleteLinearOrder.mk LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT
                  @[simp]
                  theorem toDual_sSup {α : Type u_1} [SupSet α] (s : Set α) :
                  OrderDual.toDual (sSup s) = sInf (OrderDual.ofDual ⁻¹' s)
                  @[simp]
                  theorem toDual_sInf {α : Type u_1} [InfSet α] (s : Set α) :
                  OrderDual.toDual (sInf s) = sSup (OrderDual.ofDual ⁻¹' s)
                  @[simp]
                  theorem ofDual_sSup {α : Type u_1} [InfSet α] (s : Set αᵒᵈ) :
                  OrderDual.ofDual (sSup s) = sInf (OrderDual.toDual ⁻¹' s)
                  @[simp]
                  theorem ofDual_sInf {α : Type u_1} [SupSet α] (s : Set αᵒᵈ) :
                  OrderDual.ofDual (sInf s) = sSup (OrderDual.toDual ⁻¹' s)
                  @[simp]
                  theorem toDual_iSup {α : Type u_1} {ι : Sort u_4} [SupSet α] (f : ια) :
                  OrderDual.toDual (⨆ (i : ι), f i) = ⨅ (i : ι), OrderDual.toDual (f i)
                  @[simp]
                  theorem toDual_iInf {α : Type u_1} {ι : Sort u_4} [InfSet α] (f : ια) :
                  OrderDual.toDual (⨅ (i : ι), f i) = ⨆ (i : ι), OrderDual.toDual (f i)
                  @[simp]
                  theorem ofDual_iSup {α : Type u_1} {ι : Sort u_4} [InfSet α] (f : ιαᵒᵈ) :
                  OrderDual.ofDual (⨆ (i : ι), f i) = ⨅ (i : ι), OrderDual.ofDual (f i)
                  @[simp]
                  theorem ofDual_iInf {α : Type u_1} {ι : Sort u_4} [SupSet α] (f : ιαᵒᵈ) :
                  OrderDual.ofDual (⨅ (i : ι), f i) = ⨆ (i : ι), OrderDual.ofDual (f i)
                  theorem sInf_le_sSup {α : Type u_1} [CompleteLattice α] {s : Set α} (hs : s.Nonempty) :
                  theorem sSup_union {α : Type u_1} [CompleteLattice α] {s : Set α} {t : Set α} :
                  sSup (s t) = sSup s sSup t
                  theorem sInf_union {α : Type u_1} [CompleteLattice α] {s : Set α} {t : Set α} :
                  sInf (s t) = sInf s sInf t
                  theorem sSup_inter_le {α : Type u_1} [CompleteLattice α] {s : Set α} {t : Set α} :
                  sSup (s t) sSup s sSup t
                  theorem le_sInf_inter {α : Type u_1} [CompleteLattice α] {s : Set α} {t : Set α} :
                  sInf s sInf t sInf (s t)
                  @[simp]
                  theorem sSup_empty {α : Type u_1} [CompleteLattice α] :
                  @[simp]
                  theorem sInf_empty {α : Type u_1} [CompleteLattice α] :
                  @[simp]
                  theorem sSup_univ {α : Type u_1} [CompleteLattice α] :
                  sSup Set.univ =
                  @[simp]
                  theorem sInf_univ {α : Type u_1} [CompleteLattice α] :
                  sInf Set.univ =
                  @[simp]
                  theorem sSup_insert {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} :
                  sSup (insert a s) = a sSup s
                  @[simp]
                  theorem sInf_insert {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} :
                  sInf (insert a s) = a sInf s
                  theorem sSup_le_sSup_of_subset_insert_bot {α : Type u_1} [CompleteLattice α] {s : Set α} {t : Set α} (h : s insert t) :
                  theorem sInf_le_sInf_of_subset_insert_top {α : Type u_1} [CompleteLattice α] {s : Set α} {t : Set α} (h : s insert t) :
                  @[simp]
                  theorem sSup_diff_singleton_bot {α : Type u_1} [CompleteLattice α] (s : Set α) :
                  sSup (s \ {}) = sSup s
                  @[simp]
                  theorem sInf_diff_singleton_top {α : Type u_1} [CompleteLattice α] (s : Set α) :
                  sInf (s \ {}) = sInf s
                  theorem sSup_pair {α : Type u_1} [CompleteLattice α] {a : α} {b : α} :
                  sSup {a, b} = a b
                  theorem sInf_pair {α : Type u_1} [CompleteLattice α] {a : α} {b : α} :
                  sInf {a, b} = a b
                  @[simp]
                  theorem sSup_eq_bot {α : Type u_1} [CompleteLattice α] {s : Set α} :
                  sSup s = as, a =
                  @[simp]
                  theorem sInf_eq_top {α : Type u_1} [CompleteLattice α] {s : Set α} :
                  sInf s = as, a =
                  theorem sSup_eq_bot' {α : Type u_1} [CompleteLattice α] {s : Set α} :
                  sSup s = s = s = {}
                  theorem eq_singleton_bot_of_sSup_eq_bot_of_nonempty {α : Type u_1} [CompleteLattice α] {s : Set α} (h_sup : sSup s = ) (hne : s.Nonempty) :
                  s = {}
                  theorem eq_singleton_top_of_sInf_eq_top_of_nonempty {α : Type u_1} [CompleteLattice α] {s : Set α} :
                  sInf s = s.Nonemptys = {}
                  theorem sSup_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} [CompleteLattice α] {s : Set α} {b : α} (h₁ : as, a b) (h₂ : w < b, as, w < a) :
                  sSup s = b

                  Introduction rule to prove that b is the supremum of s: it suffices to check that b is larger than all elements of s, and that this is not the case of any w < b. See csSup_eq_of_forall_le_of_forall_lt_exists_gt for a version in conditionally complete lattices.

                  theorem sInf_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} [CompleteLattice α] {s : Set α} {b : α} :
                  (∀ as, b a)(∀ (w : α), b < was, a < w)sInf s = b

                  Introduction rule to prove that b is the infimum of s: it suffices to check that b is smaller than all elements of s, and that this is not the case of any w > b. See csInf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in conditionally complete lattices.

                  theorem lt_sSup_iff {α : Type u_1} [CompleteLinearOrder α] {s : Set α} {b : α} :
                  b < sSup s as, b < a
                  theorem sInf_lt_iff {α : Type u_1} [CompleteLinearOrder α] {s : Set α} {b : α} :
                  sInf s < b as, a < b
                  theorem sSup_eq_top {α : Type u_1} [CompleteLinearOrder α] {s : Set α} :
                  sSup s = b < , as, b < a
                  theorem sInf_eq_bot {α : Type u_1} [CompleteLinearOrder α] {s : Set α} :
                  sInf s = b > , as, a < b
                  theorem lt_iSup_iff {α : Type u_1} {ι : Sort u_4} [CompleteLinearOrder α] {a : α} {f : ια} :
                  a < iSup f ∃ (i : ι), a < f i
                  theorem iInf_lt_iff {α : Type u_1} {ι : Sort u_4} [CompleteLinearOrder α] {a : α} {f : ια} :
                  iInf f < a ∃ (i : ι), f i < a
                  theorem sSup_range {α : Type u_1} {ι : Sort u_4} [SupSet α] {f : ια} :
                  theorem sSup_eq_iSup' {α : Type u_1} [SupSet α] (s : Set α) :
                  sSup s = ⨆ (a : s), a
                  theorem iSup_congr {α : Type u_1} {ι : Sort u_4} [SupSet α] {f : ια} {g : ια} (h : ∀ (i : ι), f i = g i) :
                  ⨆ (i : ι), f i = ⨆ (i : ι), g i
                  theorem biSup_congr {α : Type u_1} {ι : Sort u_4} [SupSet α] {f : ια} {g : ια} {p : ιProp} (h : ∀ (i : ι), p if i = g i) :
                  ⨆ (i : ι), ⨆ (_ : p i), f i = ⨆ (i : ι), ⨆ (_ : p i), g i
                  theorem biSup_congr' {α : Type u_1} {ι : Sort u_4} [SupSet α] {p : ιProp} {f : (i : ι) → p iα} {g : (i : ι) → p iα} (h : ∀ (i : ι) (hi : p i), f i hi = g i hi) :
                  ⨆ (i : ι), ⨆ (hi : p i), f i hi = ⨆ (i : ι), ⨆ (hi : p i), g i hi
                  theorem Function.Surjective.iSup_comp {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [SupSet α] {f : ιι'} (hf : Function.Surjective f) (g : ι'α) :
                  ⨆ (x : ι), g (f x) = ⨆ (y : ι'), g y
                  theorem Equiv.iSup_comp {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [SupSet α] {g : ι'α} (e : ι ι') :
                  ⨆ (x : ι), g (e x) = ⨆ (y : ι'), g y
                  theorem Function.Surjective.iSup_congr {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [SupSet α] {f : ια} {g : ι'α} (h : ιι') (h1 : Function.Surjective h) (h2 : ∀ (x : ι), g (h x) = f x) :
                  ⨆ (x : ι), f x = ⨆ (y : ι'), g y
                  theorem Equiv.iSup_congr {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [SupSet α] {f : ια} {g : ι'α} (e : ι ι') (h : ∀ (x : ι), g (e x) = f x) :
                  ⨆ (x : ι), f x = ⨆ (y : ι'), g y
                  theorem iSup_congr_Prop {α : Type u_1} [SupSet α] {p : Prop} {q : Prop} {f₁ : pα} {f₂ : qα} (pq : p q) (f : ∀ (x : q), f₁ = f₂ x) :
                  iSup f₁ = iSup f₂
                  theorem iSup_plift_up {α : Type u_1} {ι : Sort u_4} [SupSet α] (f : PLift ια) :
                  ⨆ (i : ι), f { down := i } = ⨆ (i : PLift ι), f i
                  theorem iSup_plift_down {α : Type u_1} {ι : Sort u_4} [SupSet α] (f : ια) :
                  ⨆ (i : PLift ι), f i.down = ⨆ (i : ι), f i
                  theorem iSup_range' {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [SupSet α] (g : βα) (f : ιβ) :
                  ⨆ (b : (Set.range f)), g b = ⨆ (i : ι), g (f i)
                  theorem sSup_image' {α : Type u_1} {β : Type u_2} [SupSet α] {s : Set β} {f : βα} :
                  sSup (f '' s) = ⨆ (a : s), f a
                  theorem sInf_range {α : Type u_1} {ι : Sort u_4} [InfSet α] {f : ια} :
                  theorem sInf_eq_iInf' {α : Type u_1} [InfSet α] (s : Set α) :
                  sInf s = ⨅ (a : s), a
                  theorem iInf_congr {α : Type u_1} {ι : Sort u_4} [InfSet α] {f : ια} {g : ια} (h : ∀ (i : ι), f i = g i) :
                  ⨅ (i : ι), f i = ⨅ (i : ι), g i
                  theorem biInf_congr {α : Type u_1} {ι : Sort u_4} [InfSet α] {f : ια} {g : ια} {p : ιProp} (h : ∀ (i : ι), p if i = g i) :
                  ⨅ (i : ι), ⨅ (_ : p i), f i = ⨅ (i : ι), ⨅ (_ : p i), g i
                  theorem biInf_congr' {α : Type u_1} {ι : Sort u_4} [InfSet α] {p : ιProp} {f : (i : ι) → p iα} {g : (i : ι) → p iα} (h : ∀ (i : ι) (hi : p i), f i hi = g i hi) :
                  ⨅ (i : ι), ⨅ (hi : p i), f i hi = ⨅ (i : ι), ⨅ (hi : p i), g i hi
                  theorem Function.Surjective.iInf_comp {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [InfSet α] {f : ιι'} (hf : Function.Surjective f) (g : ι'α) :
                  ⨅ (x : ι), g (f x) = ⨅ (y : ι'), g y
                  theorem Equiv.iInf_comp {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [InfSet α] {g : ι'α} (e : ι ι') :
                  ⨅ (x : ι), g (e x) = ⨅ (y : ι'), g y
                  theorem Function.Surjective.iInf_congr {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [InfSet α] {f : ια} {g : ι'α} (h : ιι') (h1 : Function.Surjective h) (h2 : ∀ (x : ι), g (h x) = f x) :
                  ⨅ (x : ι), f x = ⨅ (y : ι'), g y
                  theorem Equiv.iInf_congr {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [InfSet α] {f : ια} {g : ι'α} (e : ι ι') (h : ∀ (x : ι), g (e x) = f x) :
                  ⨅ (x : ι), f x = ⨅ (y : ι'), g y
                  theorem iInf_congr_Prop {α : Type u_1} [InfSet α] {p : Prop} {q : Prop} {f₁ : pα} {f₂ : qα} (pq : p q) (f : ∀ (x : q), f₁ = f₂ x) :
                  iInf f₁ = iInf f₂
                  theorem iInf_plift_up {α : Type u_1} {ι : Sort u_4} [InfSet α] (f : PLift ια) :
                  ⨅ (i : ι), f { down := i } = ⨅ (i : PLift ι), f i
                  theorem iInf_plift_down {α : Type u_1} {ι : Sort u_4} [InfSet α] (f : ια) :
                  ⨅ (i : PLift ι), f i.down = ⨅ (i : ι), f i
                  theorem iInf_range' {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [InfSet α] (g : βα) (f : ιβ) :
                  ⨅ (b : (Set.range f)), g b = ⨅ (i : ι), g (f i)
                  theorem sInf_image' {α : Type u_1} {β : Type u_2} [InfSet α] {s : Set β} {f : βα} :
                  sInf (f '' s) = ⨅ (a : s), f a
                  theorem le_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ια) (i : ι) :
                  f i iSup f
                  theorem iInf_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ια) (i : ι) :
                  iInf f f i
                  theorem le_iSup' {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ια) (i : ι) :
                  f i iSup f
                  theorem iInf_le' {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ια) (i : ι) :
                  iInf f f i
                  theorem isLUB_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} :
                  IsLUB (Set.range f) (⨆ (j : ι), f j)
                  theorem isGLB_iInf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} :
                  IsGLB (Set.range f) (⨅ (j : ι), f j)
                  theorem IsLUB.iSup_eq {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {a : α} (h : IsLUB (Set.range f) a) :
                  ⨆ (j : ι), f j = a
                  theorem IsGLB.iInf_eq {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {a : α} (h : IsGLB (Set.range f) a) :
                  ⨅ (j : ι), f j = a
                  theorem le_iSup_of_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {a : α} (i : ι) (h : a f i) :
                  a iSup f
                  theorem iInf_le_of_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {a : α} (i : ι) (h : f i a) :
                  iInf f a
                  theorem le_iSup₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] {f : (i : ι) → κ iα} (i : ι) (j : κ i) :
                  f i j ⨆ (i : ι), ⨆ (j : κ i), f i j
                  theorem iInf₂_le {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] {f : (i : ι) → κ iα} (i : ι) (j : κ i) :
                  ⨅ (i : ι), ⨅ (j : κ i), f i j f i j
                  theorem le_iSup₂_of_le {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] {a : α} {f : (i : ι) → κ iα} (i : ι) (j : κ i) (h : a f i j) :
                  a ⨆ (i : ι), ⨆ (j : κ i), f i j
                  theorem iInf₂_le_of_le {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] {a : α} {f : (i : ι) → κ iα} (i : ι) (j : κ i) (h : f i j a) :
                  ⨅ (i : ι), ⨅ (j : κ i), f i j a
                  theorem iSup_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {a : α} (h : ∀ (i : ι), f i a) :
                  iSup f a
                  theorem le_iInf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {a : α} (h : ∀ (i : ι), a f i) :
                  a iInf f
                  theorem iSup₂_le {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] {a : α} {f : (i : ι) → κ iα} (h : ∀ (i : ι) (j : κ i), f i j a) :
                  ⨆ (i : ι), ⨆ (j : κ i), f i j a
                  theorem le_iInf₂ {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] {a : α} {f : (i : ι) → κ iα} (h : ∀ (i : ι) (j : κ i), a f i j) :
                  a ⨅ (i : ι), ⨅ (j : κ i), f i j
                  theorem iSup₂_le_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (κ : ιSort u_8) (f : ια) :
                  ⨆ (i : ι), ⨆ (x : κ i), f i ⨆ (i : ι), f i
                  theorem iInf_le_iInf₂ {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (κ : ιSort u_8) (f : ια) :
                  ⨅ (i : ι), f i ⨅ (i : ι), ⨅ (x : κ i), f i
                  theorem iSup_mono {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {g : ια} (h : ∀ (i : ι), f i g i) :
                  theorem iInf_mono {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {g : ια} (h : ∀ (i : ι), f i g i) :
                  theorem iSup₂_mono {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] {f : (i : ι) → κ iα} {g : (i : ι) → κ iα} (h : ∀ (i : ι) (j : κ i), f i j g i j) :
                  ⨆ (i : ι), ⨆ (j : κ i), f i j ⨆ (i : ι), ⨆ (j : κ i), g i j
                  theorem iInf₂_mono {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] {f : (i : ι) → κ iα} {g : (i : ι) → κ iα} (h : ∀ (i : ι) (j : κ i), f i j g i j) :
                  ⨅ (i : ι), ⨅ (j : κ i), f i j ⨅ (i : ι), ⨅ (j : κ i), g i j
                  theorem iSup_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] {f : ια} {g : ι'α} (h : ∀ (i : ι), ∃ (i' : ι'), f i g i') :
                  theorem iInf_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] {f : ια} {g : ι'α} (h : ∀ (i' : ι'), ∃ (i : ι), f i g i') :
                  theorem iSup₂_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {κ : ιSort u_6} {κ' : ι'Sort u_7} [CompleteLattice α] {f : (i : ι) → κ iα} {g : (i' : ι') → κ' i'α} (h : ∀ (i : ι) (j : κ i), ∃ (i' : ι') (j' : κ' i'), f i j g i' j') :
                  ⨆ (i : ι), ⨆ (j : κ i), f i j ⨆ (i : ι'), ⨆ (j : κ' i), g i j
                  theorem iInf₂_mono' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {κ : ιSort u_6} {κ' : ι'Sort u_7} [CompleteLattice α] {f : (i : ι) → κ iα} {g : (i' : ι') → κ' i'α} (h : ∀ (i : ι') (j : κ' i), ∃ (i' : ι) (j' : κ i'), f i' j' g i j) :
                  ⨅ (i : ι), ⨅ (j : κ i), f i j ⨅ (i : ι'), ⨅ (j : κ' i), g i j
                  theorem iSup_const_mono {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] {a : α} (h : ιι') :
                  ⨆ (x : ι), a ⨆ (x : ι'), a
                  theorem iInf_const_mono {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] {a : α} (h : ι'ι) :
                  ⨅ (x : ι), a ⨅ (x : ι'), a
                  theorem iSup_iInf_le_iInf_iSup {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] (f : ιι'α) :
                  ⨆ (i : ι), ⨅ (j : ι'), f i j ⨅ (j : ι'), ⨆ (i : ι), f i j
                  theorem biSup_mono {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {p : ιProp} {q : ιProp} (hpq : ∀ (i : ι), p iq i) :
                  ⨆ (i : ι), ⨆ (_ : p i), f i ⨆ (i : ι), ⨆ (_ : q i), f i
                  theorem biInf_mono {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {p : ιProp} {q : ιProp} (hpq : ∀ (i : ι), p iq i) :
                  ⨅ (i : ι), ⨅ (_ : q i), f i ⨅ (i : ι), ⨅ (_ : p i), f i
                  @[simp]
                  theorem iSup_le_iff {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {a : α} :
                  iSup f a ∀ (i : ι), f i a
                  @[simp]
                  theorem le_iInf_iff {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {a : α} :
                  a iInf f ∀ (i : ι), a f i
                  theorem iSup₂_le_iff {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] {a : α} {f : (i : ι) → κ iα} :
                  ⨆ (i : ι), ⨆ (j : κ i), f i j a ∀ (i : ι) (j : κ i), f i j a
                  theorem le_iInf₂_iff {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] {a : α} {f : (i : ι) → κ iα} :
                  a ⨅ (i : ι), ⨅ (j : κ i), f i j ∀ (i : ι) (j : κ i), a f i j
                  theorem iSup_lt_iff {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {a : α} :
                  iSup f < a b < a, ∀ (i : ι), f i b
                  theorem lt_iInf_iff {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {a : α} :
                  a < iInf f ∃ (b : α), a < b ∀ (i : ι), b f i
                  theorem sSup_eq_iSup {α : Type u_1} [CompleteLattice α] {s : Set α} :
                  sSup s = as, a
                  theorem sInf_eq_iInf {α : Type u_1} [CompleteLattice α] {s : Set α} :
                  sInf s = as, a
                  theorem Monotone.le_map_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {s : ια} [CompleteLattice β] {f : αβ} (hf : Monotone f) :
                  ⨆ (i : ι), f (s i) f (iSup s)
                  theorem Antitone.le_map_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {s : ια} [CompleteLattice β] {f : αβ} (hf : Antitone f) :
                  ⨆ (i : ι), f (s i) f (iInf s)
                  theorem Monotone.le_map_iSup₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] [CompleteLattice β] {f : αβ} (hf : Monotone f) (s : (i : ι) → κ iα) :
                  ⨆ (i : ι), ⨆ (j : κ i), f (s i j) f (⨆ (i : ι), ⨆ (j : κ i), s i j)
                  theorem Antitone.le_map_iInf₂ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] [CompleteLattice β] {f : αβ} (hf : Antitone f) (s : (i : ι) → κ iα) :
                  ⨆ (i : ι), ⨆ (j : κ i), f (s i j) f (⨅ (i : ι), ⨅ (j : κ i), s i j)
                  theorem Monotone.le_map_sSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : αβ} (hf : Monotone f) :
                  as, f a f (sSup s)
                  theorem Antitone.le_map_sInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : αβ} (hf : Antitone f) :
                  as, f a f (sInf s)
                  theorem OrderIso.map_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (x : ια) :
                  f (⨆ (i : ι), x i) = ⨆ (i : ι), f (x i)
                  theorem OrderIso.map_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (x : ια) :
                  f (⨅ (i : ι), x i) = ⨅ (i : ι), f (x i)
                  theorem OrderIso.map_sSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (s : Set α) :
                  f (sSup s) = as, f a
                  theorem OrderIso.map_sInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (s : Set α) :
                  f (sInf s) = as, f a
                  theorem iSup_comp_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {ι' : Sort u_8} (f : ι'α) (g : ιι') :
                  ⨆ (x : ι), f (g x) ⨆ (y : ι'), f y
                  theorem le_iInf_comp {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {ι' : Sort u_8} (f : ι'α) (g : ιι') :
                  ⨅ (y : ι'), f y ⨅ (x : ι), f (g x)
                  theorem Monotone.iSup_comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] [Preorder β] {f : βα} (hf : Monotone f) {s : ιβ} (hs : ∀ (x : β), ∃ (i : ι), x s i) :
                  ⨆ (x : ι), f (s x) = ⨆ (y : β), f y
                  theorem Monotone.iInf_comp_eq {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] [Preorder β] {f : βα} (hf : Monotone f) {s : ιβ} (hs : ∀ (x : β), ∃ (i : ι), s i x) :
                  ⨅ (x : ι), f (s x) = ⨅ (y : β), f y
                  theorem Antitone.map_iSup_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {s : ια} [CompleteLattice β] {f : αβ} (hf : Antitone f) :
                  f (iSup s) ⨅ (i : ι), f (s i)
                  theorem Monotone.map_iInf_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {s : ια} [CompleteLattice β] {f : αβ} (hf : Monotone f) :
                  f (iInf s) ⨅ (i : ι), f (s i)
                  theorem Antitone.map_iSup₂_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] [CompleteLattice β] {f : αβ} (hf : Antitone f) (s : (i : ι) → κ iα) :
                  f (⨆ (i : ι), ⨆ (j : κ i), s i j) ⨅ (i : ι), ⨅ (j : κ i), f (s i j)
                  theorem Monotone.map_iInf₂_le {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] [CompleteLattice β] {f : αβ} (hf : Monotone f) (s : (i : ι) → κ iα) :
                  f (⨅ (i : ι), ⨅ (j : κ i), s i j) ⨅ (i : ι), ⨅ (j : κ i), f (s i j)
                  theorem Antitone.map_sSup_le {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : αβ} (hf : Antitone f) :
                  f (sSup s) as, f a
                  theorem Monotone.map_sInf_le {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] {s : Set α} {f : αβ} (hf : Monotone f) :
                  f (sInf s) as, f a
                  theorem iSup_const_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {a : α} :
                  ⨆ (x : ι), a a
                  theorem le_iInf_const {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {a : α} :
                  a ⨅ (x : ι), a
                  theorem iSup_const {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {a : α} [Nonempty ι] :
                  ⨆ (x : ι), a = a
                  theorem iInf_const {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {a : α} [Nonempty ι] :
                  ⨅ (x : ι), a = a
                  theorem iSup_unique {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [Unique ι] (f : ια) :
                  ⨆ (i : ι), f i = f default
                  theorem iInf_unique {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [Unique ι] (f : ια) :
                  ⨅ (i : ι), f i = f default
                  @[simp]
                  theorem iSup_bot {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] :
                  ⨆ (x : ι), =
                  @[simp]
                  theorem iInf_top {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] :
                  ⨅ (x : ι), =
                  @[simp]
                  theorem iSup_eq_bot {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {s : ια} :
                  iSup s = ∀ (i : ι), s i =
                  @[simp]
                  theorem iInf_eq_top {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {s : ια} :
                  iInf s = ∀ (i : ι), s i =
                  @[simp]
                  theorem bot_lt_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {s : ια} :
                  < ⨆ (i : ι), s i ∃ (i : ι), < s i
                  @[simp]
                  theorem iInf_lt_top {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {s : ια} :
                  ⨅ (i : ι), s i < ∃ (i : ι), s i <
                  theorem iSup₂_eq_bot {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] {f : (i : ι) → κ iα} :
                  ⨆ (i : ι), ⨆ (j : κ i), f i j = ∀ (i : ι) (j : κ i), f i j =
                  theorem iInf₂_eq_top {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLattice α] {f : (i : ι) → κ iα} :
                  ⨅ (i : ι), ⨅ (j : κ i), f i j = ∀ (i : ι) (j : κ i), f i j =
                  @[simp]
                  theorem iSup_pos {α : Type u_1} [CompleteLattice α] {p : Prop} {f : pα} (hp : p) :
                  ⨆ (h : p), f h = f hp
                  @[simp]
                  theorem iInf_pos {α : Type u_1} [CompleteLattice α] {p : Prop} {f : pα} (hp : p) :
                  ⨅ (h : p), f h = f hp
                  @[simp]
                  theorem iSup_neg {α : Type u_1} [CompleteLattice α] {p : Prop} {f : pα} (hp : ¬p) :
                  ⨆ (h : p), f h =
                  @[simp]
                  theorem iInf_neg {α : Type u_1} [CompleteLattice α] {p : Prop} {f : pα} (hp : ¬p) :
                  ⨅ (h : p), f h =
                  theorem iSup_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {b : α} {f : ια} (h₁ : ∀ (i : ι), f i b) (h₂ : w < b, ∃ (i : ι), w < f i) :
                  ⨆ (i : ι), f i = b

                  Introduction rule to prove that b is the supremum of f: it suffices to check that b is larger than f i for all i, and that this is not the case of any w<b. See ciSup_eq_of_forall_le_of_forall_lt_exists_gt for a version in conditionally complete lattices.

                  theorem iInf_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {b : α} :
                  (∀ (i : ι), b f i)(∀ (w : α), b < w∃ (i : ι), f i < w)⨅ (i : ι), f i = b

                  Introduction rule to prove that b is the infimum of f: it suffices to check that b is smaller than f i for all i, and that this is not the case of any w>b. See ciInf_eq_of_forall_ge_of_forall_gt_exists_lt for a version in conditionally complete lattices.

                  theorem iSup_eq_dif {α : Type u_1} [CompleteLattice α] {p : Prop} [Decidable p] (a : pα) :
                  ⨆ (h : p), a h = if h : p then a h else
                  theorem iSup_eq_if {α : Type u_1} [CompleteLattice α] {p : Prop} [Decidable p] (a : α) :
                  ⨆ (_ : p), a = if p then a else
                  theorem iInf_eq_dif {α : Type u_1} [CompleteLattice α] {p : Prop} [Decidable p] (a : pα) :
                  ⨅ (h : p), a h = if h : p then a h else
                  theorem iInf_eq_if {α : Type u_1} [CompleteLattice α] {p : Prop} [Decidable p] (a : α) :
                  ⨅ (_ : p), a = if p then a else
                  theorem iSup_comm {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] {f : ιι'α} :
                  ⨆ (i : ι), ⨆ (j : ι'), f i j = ⨆ (j : ι'), ⨆ (i : ι), f i j
                  theorem iInf_comm {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [CompleteLattice α] {f : ιι'α} :
                  ⨅ (i : ι), ⨅ (j : ι'), f i j = ⨅ (j : ι'), ⨅ (i : ι), f i j
                  theorem iSup₂_comm {α : Type u_1} [CompleteLattice α] {ι₁ : Sort u_8} {ι₂ : Sort u_9} {κ₁ : ι₁Sort u_10} {κ₂ : ι₂Sort u_11} (f : (i₁ : ι₁) → κ₁ i₁(i₂ : ι₂) → κ₂ i₂α) :
                  ⨆ (i₁ : ι₁), ⨆ (j₁ : κ₁ i₁), ⨆ (i₂ : ι₂), ⨆ (j₂ : κ₂ i₂), f i₁ j₁ i₂ j₂ = ⨆ (i₂ : ι₂), ⨆ (j₂ : κ₂ i₂), ⨆ (i₁ : ι₁), ⨆ (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂
                  theorem iInf₂_comm {α : Type u_1} [CompleteLattice α] {ι₁ : Sort u_8} {ι₂ : Sort u_9} {κ₁ : ι₁Sort u_10} {κ₂ : ι₂Sort u_11} (f : (i₁ : ι₁) → κ₁ i₁(i₂ : ι₂) → κ₂ i₂α) :
                  ⨅ (i₁ : ι₁), ⨅ (j₁ : κ₁ i₁), ⨅ (i₂ : ι₂), ⨅ (j₂ : κ₂ i₂), f i₁ j₁ i₂ j₂ = ⨅ (i₂ : ι₂), ⨅ (j₂ : κ₂ i₂), ⨅ (i₁ : ι₁), ⨅ (j₁ : κ₁ i₁), f i₁ j₁ i₂ j₂
                  @[simp]
                  theorem iSup_iSup_eq_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {b : β} {f : (x : β) → x = bα} :
                  ⨆ (x : β), ⨆ (h : x = b), f x h = f b
                  @[simp]
                  theorem iInf_iInf_eq_left {α : Type u_1} {β : Type u_2} [CompleteLattice α] {b : β} {f : (x : β) → x = bα} :
                  ⨅ (x : β), ⨅ (h : x = b), f x h = f b
                  @[simp]
                  theorem iSup_iSup_eq_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {b : β} {f : (x : β) → b = xα} :
                  ⨆ (x : β), ⨆ (h : b = x), f x h = f b
                  @[simp]
                  theorem iInf_iInf_eq_right {α : Type u_1} {β : Type u_2} [CompleteLattice α] {b : β} {f : (x : β) → b = xα} :
                  ⨅ (x : β), ⨅ (h : b = x), f x h = f b
                  theorem iSup_subtype {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ιProp} {f : Subtype pα} :
                  iSup f = ⨆ (i : ι), ⨆ (h : p i), f i, h
                  theorem iInf_subtype {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ιProp} {f : Subtype pα} :
                  iInf f = ⨅ (i : ι), ⨅ (h : p i), f i, h
                  theorem iSup_subtype' {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ιProp} {f : (i : ι) → p iα} :
                  ⨆ (i : ι), ⨆ (h : p i), f i h = ⨆ (x : Subtype p), f x
                  theorem iInf_subtype' {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ιProp} {f : (i : ι) → p iα} :
                  ⨅ (i : ι), ⨅ (h : p i), f i h = ⨅ (x : Subtype p), f x
                  theorem iSup_subtype'' {α : Type u_1} [CompleteLattice α] {ι : Type u_8} (s : Set ι) (f : ια) :
                  ⨆ (i : s), f i = ts, f t
                  theorem iInf_subtype'' {α : Type u_1} [CompleteLattice α] {ι : Type u_8} (s : Set ι) (f : ια) :
                  ⨅ (i : s), f i = ts, f t
                  theorem biSup_const {α : Type u_1} [CompleteLattice α] {ι : Type u_8} {a : α} {s : Set ι} (hs : s.Nonempty) :
                  is, a = a
                  theorem biInf_const {α : Type u_1} [CompleteLattice α] {ι : Type u_8} {a : α} {s : Set ι} (hs : s.Nonempty) :
                  is, a = a
                  theorem iSup_sup_eq {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {g : ια} :
                  ⨆ (x : ι), f x g x = (⨆ (x : ι), f x) ⨆ (x : ι), g x
                  theorem iInf_inf_eq {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {f : ια} {g : ια} :
                  ⨅ (x : ι), f x g x = (⨅ (x : ι), f x) ⨅ (x : ι), g x
                  theorem Equiv.biSup_comp {α : Type u_1} [CompleteLattice α] {ι : Type u_8} {ι' : Type u_9} {g : ι'α} (e : ι ι') (s : Set ι') :
                  ie.symm '' s, g (e i) = is, g i
                  theorem Equiv.biInf_comp {α : Type u_1} [CompleteLattice α] {ι : Type u_8} {ι' : Type u_9} {g : ι'α} (e : ι ι') (s : Set ι') :
                  ie.symm '' s, g (e i) = is, g i
                  theorem biInf_le {α : Type u_1} [CompleteLattice α] {ι : Type u_8} {s : Set ι} (f : ια) {i : ι} (hi : i s) :
                  is, f i f i
                  theorem le_biSup {α : Type u_1} [CompleteLattice α] {ι : Type u_8} {s : Set ι} (f : ια) {i : ι} (hi : i s) :
                  f i is, f i
                  theorem iSup_sup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [Nonempty ι] {f : ια} {a : α} :
                  (⨆ (x : ι), f x) a = ⨆ (x : ι), f x a
                  theorem iInf_inf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [Nonempty ι] {f : ια} {a : α} :
                  (⨅ (x : ι), f x) a = ⨅ (x : ι), f x a
                  theorem sup_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [Nonempty ι] {f : ια} {a : α} :
                  a ⨆ (x : ι), f x = ⨆ (x : ι), a f x
                  theorem inf_iInf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [Nonempty ι] {f : ια} {a : α} :
                  a ⨅ (x : ι), f x = ⨅ (x : ι), a f x
                  theorem biSup_sup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ιProp} {f : (i : ι) → p iα} {a : α} (h : ∃ (i : ι), p i) :
                  (⨆ (i : ι), ⨆ (h : p i), f i h) a = ⨆ (i : ι), ⨆ (h : p i), f i h a
                  theorem sup_biSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ιProp} {f : (i : ι) → p iα} {a : α} (h : ∃ (i : ι), p i) :
                  a ⨆ (i : ι), ⨆ (h : p i), f i h = ⨆ (i : ι), ⨆ (h : p i), a f i h
                  theorem biInf_inf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ιProp} {f : (i : ι) → p iα} {a : α} (h : ∃ (i : ι), p i) :
                  (⨅ (i : ι), ⨅ (h : p i), f i h) a = ⨅ (i : ι), ⨅ (h : p i), f i h a
                  theorem inf_biInf {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ιProp} {f : (i : ι) → p iα} {a : α} (h : ∃ (i : ι), p i) :
                  a ⨅ (i : ι), ⨅ (h : p i), f i h = ⨅ (i : ι), ⨅ (h : p i), a f i h
                  theorem biSup_lt_eq_iSup {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [LT ι] [NoMaxOrder ι] {f : ια} :
                  ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j = ⨆ (i : ι), f i
                  theorem biSup_le_eq_iSup {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [Preorder ι] {f : ια} :
                  ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j i), f j = ⨆ (i : ι), f i
                  theorem biInf_lt_eq_iInf {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [LT ι] [NoMaxOrder ι] {f : ια} :
                  ⨅ (i : ι), ⨅ (j : ι), ⨅ (_ : j < i), f j = ⨅ (i : ι), f i
                  theorem biInf_le_eq_iInf {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [Preorder ι] {f : ια} :
                  ⨅ (i : ι), ⨅ (j : ι), ⨅ (_ : j i), f j = ⨅ (i : ι), f i
                  theorem biSup_gt_eq_iSup {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [LT ι] [NoMinOrder ι] {f : ια} :
                  ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j = ⨆ (i : ι), f i
                  theorem biSup_ge_eq_iSup {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [Preorder ι] {f : ια} :
                  ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j i), f j = ⨆ (i : ι), f i
                  theorem biInf_gt_eq_iInf {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [LT ι] [NoMinOrder ι] {f : ια} :
                  ⨅ (i : ι), ⨅ (j : ι), ⨅ (_ : j > i), f j = ⨅ (i : ι), f i
                  theorem biInf_ge_eq_iInf {α : Type u_1} [CompleteLattice α] {ι : Type u_8} [Preorder ι] {f : ια} :
                  ⨅ (i : ι), ⨅ (j : ι), ⨅ (_ : j i), f j = ⨅ (i : ι), f i

                  iSup and iInf under Prop #

                  theorem iSup_false {α : Type u_1} [CompleteLattice α] {s : Falseα} :
                  theorem iInf_false {α : Type u_1} [CompleteLattice α] {s : Falseα} :
                  theorem iSup_true {α : Type u_1} [CompleteLattice α] {s : Trueα} :
                  theorem iInf_true {α : Type u_1} [CompleteLattice α] {s : Trueα} :
                  @[simp]
                  theorem iSup_exists {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ιProp} {f : Exists pα} :
                  ⨆ (x : Exists p), f x = ⨆ (i : ι), ⨆ (h : p i), f
                  @[simp]
                  theorem iInf_exists {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] {p : ιProp} {f : Exists pα} :
                  ⨅ (x : Exists p), f x = ⨅ (i : ι), ⨅ (h : p i), f
                  theorem iSup_and {α : Type u_1} [CompleteLattice α] {p : Prop} {q : Prop} {s : p qα} :
                  iSup s = ⨆ (h₁ : p), ⨆ (h₂ : q), s
                  theorem iInf_and {α : Type u_1} [CompleteLattice α] {p : Prop} {q : Prop} {s : p qα} :
                  iInf s = ⨅ (h₁ : p), ⨅ (h₂ : q), s
                  theorem iSup_and' {α : Type u_1} [CompleteLattice α] {p : Prop} {q : Prop} {s : pqα} :
                  ⨆ (h₁ : p), ⨆ (h₂ : q), s h₁ h₂ = ⨆ (h : p q), s

                  The symmetric case of iSup_and, useful for rewriting into a supremum over a conjunction

                  theorem iInf_and' {α : Type u_1} [CompleteLattice α] {p : Prop} {q : Prop} {s : pqα} :
                  ⨅ (h₁ : p), ⨅ (h₂ : q), s h₁ h₂ = ⨅ (h : p q), s

                  The symmetric case of iInf_and, useful for rewriting into an infimum over a conjunction

                  theorem iSup_or {α : Type u_1} [CompleteLattice α] {p : Prop} {q : Prop} {s : p qα} :
                  ⨆ (x : p q), s x = (⨆ (i : p), s ) ⨆ (j : q), s
                  theorem iInf_or {α : Type u_1} [CompleteLattice α] {p : Prop} {q : Prop} {s : p qα} :
                  ⨅ (x : p q), s x = (⨅ (i : p), s ) ⨅ (j : q), s
                  theorem iSup_dite {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (p : ιProp) [DecidablePred p] (f : (i : ι) → p iα) (g : (i : ι) → ¬p iα) :
                  (⨆ (i : ι), if h : p i then f i h else g i h) = (⨆ (i : ι), ⨆ (h : p i), f i h) ⨆ (i : ι), ⨆ (h : ¬p i), g i h
                  theorem iInf_dite {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (p : ιProp) [DecidablePred p] (f : (i : ι) → p iα) (g : (i : ι) → ¬p iα) :
                  (⨅ (i : ι), if h : p i then f i h else g i h) = (⨅ (i : ι), ⨅ (h : p i), f i h) ⨅ (i : ι), ⨅ (h : ¬p i), g i h
                  theorem iSup_ite {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (p : ιProp) [DecidablePred p] (f : ια) (g : ια) :
                  (⨆ (i : ι), if p i then f i else g i) = (⨆ (i : ι), ⨆ (_ : p i), f i) ⨆ (i : ι), ⨆ (_ : ¬p i), g i
                  theorem iInf_ite {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (p : ιProp) [DecidablePred p] (f : ια) (g : ια) :
                  (⨅ (i : ι), if p i then f i else g i) = (⨅ (i : ι), ⨅ (_ : p i), f i) ⨅ (i : ι), ⨅ (_ : ¬p i), g i
                  theorem iSup_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {g : βα} {f : ιβ} :
                  bSet.range f, g b = ⨆ (i : ι), g (f i)
                  theorem iInf_range {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {g : βα} {f : ιβ} :
                  bSet.range f, g b = ⨅ (i : ι), g (f i)
                  theorem sSup_image {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : βα} :
                  sSup (f '' s) = as, f a
                  theorem sInf_image {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : βα} :
                  sInf (f '' s) = as, f a
                  theorem OrderIso.map_sSup_eq_sSup_symm_preimage {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (s : Set α) :
                  f (sSup s) = sSup (f.symm ⁻¹' s)
                  theorem OrderIso.map_sInf_eq_sInf_symm_preimage {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : α ≃o β) (s : Set α) :
                  f (sInf s) = sInf (f.symm ⁻¹' s)
                  theorem iSup_emptyset {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} :
                  x, f x =
                  theorem iInf_emptyset {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} :
                  x, f x =
                  theorem iSup_univ {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} :
                  xSet.univ, f x = ⨆ (x : β), f x
                  theorem iInf_univ {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} :
                  xSet.univ, f x = ⨅ (x : β), f x
                  theorem iSup_union {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} {s : Set β} {t : Set β} :
                  xs t, f x = (⨆ xs, f x) xt, f x
                  theorem iInf_union {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} {s : Set β} {t : Set β} :
                  xs t, f x = (⨅ xs, f x) xt, f x
                  theorem iSup_split {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : βα) (p : βProp) :
                  ⨆ (i : β), f i = (⨆ (i : β), ⨆ (_ : p i), f i) ⨆ (i : β), ⨆ (_ : ¬p i), f i
                  theorem iInf_split {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : βα) (p : βProp) :
                  ⨅ (i : β), f i = (⨅ (i : β), ⨅ (_ : p i), f i) ⨅ (i : β), ⨅ (_ : ¬p i), f i
                  theorem iSup_split_single {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : βα) (i₀ : β) :
                  ⨆ (i : β), f i = f i₀ ⨆ (i : β), ⨆ (_ : i i₀), f i
                  theorem iInf_split_single {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : βα) (i₀ : β) :
                  ⨅ (i : β), f i = f i₀ ⨅ (i : β), ⨅ (_ : i i₀), f i
                  theorem iSup_le_iSup_of_subset {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} {s : Set β} {t : Set β} :
                  s txs, f x xt, f x
                  theorem iInf_le_iInf_of_subset {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} {s : Set β} {t : Set β} :
                  s txt, f x xs, f x
                  theorem iSup_insert {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} {s : Set β} {b : β} :
                  xinsert b s, f x = f b xs, f x
                  theorem iInf_insert {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} {s : Set β} {b : β} :
                  xinsert b s, f x = f b xs, f x
                  theorem iSup_singleton {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} {b : β} :
                  x{b}, f x = f b
                  theorem iInf_singleton {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} {b : β} :
                  x{b}, f x = f b
                  theorem iSup_pair {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} {a : β} {b : β} :
                  x{a, b}, f x = f a f b
                  theorem iInf_pair {α : Type u_1} {β : Type u_2} [CompleteLattice α] {f : βα} {a : β} {b : β} :
                  x{a, b}, f x = f a f b
                  theorem iSup_image {α : Type u_1} {β : Type u_2} [CompleteLattice α] {γ : Type u_8} {f : βγ} {g : γα} {t : Set β} :
                  cf '' t, g c = bt, g (f b)
                  theorem iInf_image {α : Type u_1} {β : Type u_2} [CompleteLattice α] {γ : Type u_8} {f : βγ} {g : γα} {t : Set β} :
                  cf '' t, g c = bt, g (f b)
                  theorem iSup_extend_bot {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {e : ιβ} (he : Function.Injective e) (f : ια) :
                  ⨆ (j : β), Function.extend e f j = ⨆ (i : ι), f i
                  theorem iInf_extend_top {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [CompleteLattice α] {e : ιβ} (he : Function.Injective e) (f : ια) :
                  ⨅ (j : β), Function.extend e f j = iInf f

                  iSup and iInf under Type #

                  theorem iSup_of_empty' {α : Type u_8} {ι : Sort u_9} [SupSet α] [IsEmpty ι] (f : ια) :
                  theorem iInf_of_isEmpty {α : Type u_8} {ι : Sort u_9} [InfSet α] [IsEmpty ι] (f : ια) :
                  theorem iSup_of_empty {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [IsEmpty ι] (f : ια) :
                  theorem iInf_of_empty {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] [IsEmpty ι] (f : ια) :
                  theorem iSup_bool_eq {α : Type u_1} [CompleteLattice α] {f : Boolα} :
                  ⨆ (b : Bool), f b = f true f false
                  theorem iInf_bool_eq {α : Type u_1} [CompleteLattice α] {f : Boolα} :
                  ⨅ (b : Bool), f b = f true f false
                  theorem sup_eq_iSup {α : Type u_1} [CompleteLattice α] (x : α) (y : α) :
                  x y = ⨆ (b : Bool), bif b then x else y
                  theorem inf_eq_iInf {α : Type u_1} [CompleteLattice α] (x : α) (y : α) :
                  x y = ⨅ (b : Bool), bif b then x else y
                  theorem isGLB_biInf {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : βα} :
                  IsGLB (f '' s) (⨅ xs, f x)
                  theorem isLUB_biSup {α : Type u_1} {β : Type u_2} [CompleteLattice α] {s : Set β} {f : βα} :
                  IsLUB (f '' s) (⨆ xs, f x)
                  theorem iSup_sigma {α : Type u_1} {β : Type u_2} [CompleteLattice α] {p : βType u_8} {f : Sigma pα} :
                  ⨆ (x : Sigma p), f x = ⨆ (i : β), ⨆ (j : p i), f i, j
                  theorem iInf_sigma {α : Type u_1} {β : Type u_2} [CompleteLattice α] {p : βType u_8} {f : Sigma pα} :
                  ⨅ (x : Sigma p), f x = ⨅ (i : β), ⨅ (j : p i), f i, j
                  theorem iSup_sigma' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {κ : βType u_8} (f : (i : β) → κ iα) :
                  ⨆ (i : β), ⨆ (j : κ i), f i j = ⨆ (x : (i : β) × κ i), f x.fst x.snd
                  theorem iInf_sigma' {α : Type u_1} {β : Type u_2} [CompleteLattice α] {κ : βType u_8} (f : (i : β) → κ iα) :
                  ⨅ (i : β), ⨅ (j : κ i), f i j = ⨅ (x : (i : β) × κ i), f x.fst x.snd
                  theorem iSup_psigma {α : Type u_1} [CompleteLattice α] {ι : Sort u_8} {κ : ιSort u_9} (f : (i : ι) ×' κ iα) :
                  ⨆ (ij : (i : ι) ×' κ i), f ij = ⨆ (i : ι), ⨆ (j : κ i), f i, j
                  theorem iInf_psigma {α : Type u_1} [CompleteLattice α] {ι : Sort u_8} {κ : ιSort u_9} (f : (i : ι) ×' κ iα) :
                  ⨅ (ij : (i : ι) ×' κ i), f ij = ⨅ (i : ι), ⨅ (j : κ i), f i, j
                  theorem iSup_psigma' {α : Type u_1} [CompleteLattice α] {ι : Sort u_8} {κ : ιSort u_9} (f : (i : ι) → κ iα) :
                  ⨆ (i : ι), ⨆ (j : κ i), f i j = ⨆ (ij : (i : ι) ×' κ i), f ij.fst ij.snd
                  theorem iInf_psigma' {α : Type u_1} [CompleteLattice α] {ι : Sort u_8} {κ : ιSort u_9} (f : (i : ι) → κ iα) :
                  ⨅ (i : ι), ⨅ (j : κ i), f i j = ⨅ (ij : (i : ι) ×' κ i), f ij.fst ij.snd
                  theorem iSup_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β × γα} :
                  ⨆ (x : β × γ), f x = ⨆ (i : β), ⨆ (j : γ), f (i, j)
                  theorem iInf_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β × γα} :
                  ⨅ (x : β × γ), f x = ⨅ (i : β), ⨅ (j : γ), f (i, j)
                  theorem iSup_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] (f : βγα) :
                  ⨆ (i : β), ⨆ (j : γ), f i j = ⨆ (x : β × γ), f x.1 x.2
                  theorem iInf_prod' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] (f : βγα) :
                  ⨅ (i : β), ⨅ (j : γ), f i j = ⨅ (x : β × γ), f x.1 x.2
                  theorem biSup_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β × γα} {s : Set β} {t : Set γ} :
                  xs ×ˢ t, f x = as, bt, f (a, b)
                  theorem biInf_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β × γα} {s : Set β} {t : Set γ} :
                  xs ×ˢ t, f x = as, bt, f (a, b)
                  theorem iSup_image2 {α : Type u_1} {β : Type u_2} [CompleteLattice α] {γ : Type u_8} {δ : Type u_9} (f : βγδ) (s : Set β) (t : Set γ) (g : δα) :
                  dSet.image2 f s t, g d = bs, ct, g (f b c)
                  theorem iInf_image2 {α : Type u_1} {β : Type u_2} [CompleteLattice α] {γ : Type u_8} {δ : Type u_9} (f : βγδ) (s : Set β) (t : Set γ) (g : δα) :
                  dSet.image2 f s t, g d = bs, ct, g (f b c)
                  theorem iSup_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β γα} :
                  ⨆ (x : β γ), f x = (⨆ (i : β), f (Sum.inl i)) ⨆ (j : γ), f (Sum.inr j)
                  theorem iInf_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β γα} :
                  ⨅ (x : β γ), f x = (⨅ (i : β), f (Sum.inl i)) ⨅ (j : γ), f (Sum.inr j)
                  theorem iSup_option {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : Option βα) :
                  ⨆ (o : Option β), f o = f none ⨆ (b : β), f (some b)
                  theorem iInf_option {α : Type u_1} {β : Type u_2} [CompleteLattice α] (f : Option βα) :
                  ⨅ (o : Option β), f o = f none ⨅ (b : β), f (some b)
                  theorem iSup_option_elim {α : Type u_1} {β : Type u_2} [CompleteLattice α] (a : α) (f : βα) :
                  ⨆ (o : Option β), o.elim a f = a ⨆ (b : β), f b

                  A version of iSup_option useful for rewriting right-to-left.

                  theorem iInf_option_elim {α : Type u_1} {β : Type u_2} [CompleteLattice α] (a : α) (f : βα) :
                  ⨅ (o : Option β), o.elim a f = a ⨅ (b : β), f b

                  A version of iInf_option useful for rewriting right-to-left.

                  @[simp]
                  theorem iSup_ne_bot_subtype {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ια) :
                  ⨆ (i : { i : ι // f i }), f i = ⨆ (i : ι), f i

                  When taking the supremum of f : ι → α, the elements of ι on which f gives can be dropped, without changing the result.

                  theorem iInf_ne_top_subtype {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ια) :
                  ⨅ (i : { i : ι // f i }), f i = ⨅ (i : ι), f i

                  When taking the infimum of f : ι → α, the elements of ι on which f gives can be dropped, without changing the result.

                  theorem sSup_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : βγα} {s : Set β} {t : Set γ} :
                  sSup (Set.image2 f s t) = as, bt, f a b
                  theorem sInf_image2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : βγα} {s : Set β} {t : Set γ} :
                  sInf (Set.image2 f s t) = as, bt, f a b

                  iSup and iInf under #

                  theorem iSup_ge_eq_iSup_nat_add {α : Type u_1} [CompleteLattice α] (u : α) (n : ) :
                  ⨆ (i : ), ⨆ (_ : i n), u i = ⨆ (i : ), u (i + n)
                  theorem iInf_ge_eq_iInf_nat_add {α : Type u_1} [CompleteLattice α] (u : α) (n : ) :
                  ⨅ (i : ), ⨅ (_ : i n), u i = ⨅ (i : ), u (i + n)
                  theorem Monotone.iSup_nat_add {α : Type u_1} [CompleteLattice α] {f : α} (hf : Monotone f) (k : ) :
                  ⨆ (n : ), f (n + k) = ⨆ (n : ), f n
                  theorem Antitone.iInf_nat_add {α : Type u_1} [CompleteLattice α] {f : α} (hf : Antitone f) (k : ) :
                  ⨅ (n : ), f (n + k) = ⨅ (n : ), f n
                  theorem iSup_iInf_ge_nat_add {α : Type u_1} [CompleteLattice α] (f : α) (k : ) :
                  ⨆ (n : ), ⨅ (i : ), ⨅ (_ : i n), f (i + k) = ⨆ (n : ), ⨅ (i : ), ⨅ (_ : i n), f i
                  theorem iInf_iSup_ge_nat_add {α : Type u_1} [CompleteLattice α] (f : α) (k : ) :
                  ⨅ (n : ), ⨆ (i : ), ⨆ (_ : i n), f (i + k) = ⨅ (n : ), ⨆ (i : ), ⨆ (_ : i n), f i
                  theorem sup_iSup_nat_succ {α : Type u_1} [CompleteLattice α] (u : α) :
                  u 0 ⨆ (i : ), u (i + 1) = ⨆ (i : ), u i
                  theorem inf_iInf_nat_succ {α : Type u_1} [CompleteLattice α] (u : α) :
                  u 0 ⨅ (i : ), u (i + 1) = ⨅ (i : ), u i
                  theorem iInf_nat_gt_zero_eq {α : Type u_1} [CompleteLattice α] (f : α) :
                  ⨅ (i : ), ⨅ (_ : i > 0), f i = ⨅ (i : ), f (i + 1)
                  theorem iSup_nat_gt_zero_eq {α : Type u_1} [CompleteLattice α] (f : α) :
                  ⨆ (i : ), ⨆ (_ : i > 0), f i = ⨆ (i : ), f (i + 1)
                  theorem iSup_eq_top {α : Type u_1} {ι : Sort u_4} [CompleteLinearOrder α] (f : ια) :
                  iSup f = b < , ∃ (i : ι), b < f i
                  theorem iInf_eq_bot {α : Type u_1} {ι : Sort u_4} [CompleteLinearOrder α] (f : ια) :
                  iInf f = b > , ∃ (i : ι), f i < b
                  theorem iSup₂_eq_top {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLinearOrder α] (f : (i : ι) → κ iα) :
                  ⨆ (i : ι), ⨆ (j : κ i), f i j = b < , ∃ (i : ι) (j : κ i), b < f i j
                  theorem iInf₂_eq_bot {α : Type u_1} {ι : Sort u_4} {κ : ιSort u_6} [CompleteLinearOrder α] (f : (i : ι) → κ iα) :
                  ⨅ (i : ι), ⨅ (j : κ i), f i j = b > , ∃ (i : ι) (j : κ i), f i j < b

                  Instances #

                  Equations
                  • One or more equations did not get rendered due to their size.
                  @[simp]
                  theorem sSup_Prop_eq {s : Set Prop} :
                  sSup s = ps, p
                  @[simp]
                  theorem sInf_Prop_eq {s : Set Prop} :
                  sInf s = ps, p
                  @[simp]
                  theorem iSup_Prop_eq {ι : Sort u_4} {p : ιProp} :
                  ⨆ (i : ι), p i = ∃ (i : ι), p i
                  @[simp]
                  theorem iInf_Prop_eq {ι : Sort u_4} {p : ιProp} :
                  ⨅ (i : ι), p i = ∀ (i : ι), p i
                  instance Pi.supSet {α : Type u_8} {β : αType u_9} [(i : α) → SupSet (β i)] :
                  SupSet ((i : α) → β i)
                  Equations
                  • Pi.supSet = { sSup := fun (s : Set ((i : α) → β i)) (i : α) => ⨆ (f : s), f i }
                  instance Pi.infSet {α : Type u_8} {β : αType u_9} [(i : α) → InfSet (β i)] :
                  InfSet ((i : α) → β i)
                  Equations
                  • Pi.infSet = { sInf := fun (s : Set ((i : α) → β i)) (i : α) => ⨅ (f : s), f i }
                  instance Pi.instCompleteLattice {α : Type u_8} {β : αType u_9} [(i : α) → CompleteLattice (β i)] :
                  CompleteLattice ((i : α) → β i)
                  Equations
                  @[simp]
                  theorem sSup_apply {α : Type u_8} {β : αType u_9} [(i : α) → SupSet (β i)] {s : Set ((a : α) → β a)} {a : α} :
                  sSup s a = ⨆ (f : s), f a
                  @[simp]
                  theorem sInf_apply {α : Type u_8} {β : αType u_9} [(i : α) → InfSet (β i)] {s : Set ((a : α) → β a)} {a : α} :
                  sInf s a = ⨅ (f : s), f a
                  @[simp]
                  theorem iSup_apply {α : Type u_8} {β : αType u_9} {ι : Sort u_10} [(i : α) → SupSet (β i)] {f : ι(a : α) → β a} {a : α} :
                  (⨆ (i : ι), f i) a = ⨆ (i : ι), f i a
                  @[simp]
                  theorem iInf_apply {α : Type u_8} {β : αType u_9} {ι : Sort u_10} [(i : α) → InfSet (β i)] {f : ι(a : α) → β a} {a : α} :
                  (⨅ (i : ι), f i) a = ⨅ (i : ι), f i a
                  theorem unary_relation_sSup_iff {α : Type u_8} (s : Set (αProp)) {a : α} :
                  sSup s a rs, r a
                  theorem unary_relation_sInf_iff {α : Type u_8} (s : Set (αProp)) {a : α} :
                  sInf s a rs, r a
                  theorem binary_relation_sSup_iff {α : Type u_8} {β : Type u_9} (s : Set (αβProp)) {a : α} {b : β} :
                  sSup s a b rs, r a b
                  theorem binary_relation_sInf_iff {α : Type u_8} {β : Type u_9} (s : Set (αβProp)) {a : α} {b : β} :
                  sInf s a b rs, r a b
                  theorem Monotone.sSup {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (αβ)} (hs : fs, Monotone f) :
                  theorem Monotone.sInf {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (αβ)} (hs : fs, Monotone f) :
                  theorem Antitone.sSup {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (αβ)} (hs : fs, Antitone f) :
                  theorem Antitone.sInf {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (αβ)} (hs : fs, Antitone f) :
                  @[deprecated Monotone.sSup]
                  theorem monotone_sSup_of_monotone {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (αβ)} (hs : fs, Monotone f) :

                  Alias of Monotone.sSup.

                  @[deprecated Monotone.sInf]
                  theorem monotone_sInf_of_monotone {α : Type u_1} {β : Type u_2} [Preorder α] [CompleteLattice β] {s : Set (αβ)} (hs : fs, Monotone f) :

                  Alias of Monotone.sInf.

                  theorem Monotone.iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Preorder α] [CompleteLattice β] {f : ιαβ} (hf : ∀ (i : ι), Monotone (f i)) :
                  Monotone (⨆ (i : ι), f i)
                  theorem Monotone.iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Preorder α] [CompleteLattice β] {f : ιαβ} (hf : ∀ (i : ι), Monotone (f i)) :
                  Monotone (⨅ (i : ι), f i)
                  theorem Antitone.iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Preorder α] [CompleteLattice β] {f : ιαβ} (hf : ∀ (i : ι), Antitone (f i)) :
                  Antitone (⨆ (i : ι), f i)
                  theorem Antitone.iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Preorder α] [CompleteLattice β] {f : ιαβ} (hf : ∀ (i : ι), Antitone (f i)) :
                  Antitone (⨅ (i : ι), f i)
                  instance Prod.supSet (α : Type u_1) (β : Type u_2) [SupSet α] [SupSet β] :
                  SupSet (α × β)
                  Equations
                  instance Prod.infSet (α : Type u_1) (β : Type u_2) [InfSet α] [InfSet β] :
                  InfSet (α × β)
                  Equations
                  theorem Prod.fst_sInf {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] (s : Set (α × β)) :
                  (sInf s).1 = sInf (Prod.fst '' s)
                  theorem Prod.snd_sInf {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] (s : Set (α × β)) :
                  (sInf s).2 = sInf (Prod.snd '' s)
                  theorem Prod.swap_sInf {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] (s : Set (α × β)) :
                  (sInf s).swap = sInf (Prod.swap '' s)
                  theorem Prod.fst_sSup {α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] (s : Set (α × β)) :
                  (sSup s).1 = sSup (Prod.fst '' s)
                  theorem Prod.snd_sSup {α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] (s : Set (α × β)) :
                  (sSup s).2 = sSup (Prod.snd '' s)
                  theorem Prod.swap_sSup {α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] (s : Set (α × β)) :
                  (sSup s).swap = sSup (Prod.swap '' s)
                  theorem Prod.fst_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [InfSet α] [InfSet β] (f : ια × β) :
                  (iInf f).1 = ⨅ (i : ι), (f i).1
                  theorem Prod.snd_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [InfSet α] [InfSet β] (f : ια × β) :
                  (iInf f).2 = ⨅ (i : ι), (f i).2
                  theorem Prod.swap_iInf {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [InfSet α] [InfSet β] (f : ια × β) :
                  (iInf f).swap = ⨅ (i : ι), (f i).swap
                  theorem Prod.iInf_mk {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [InfSet α] [InfSet β] (f : ια) (g : ιβ) :
                  ⨅ (i : ι), (f i, g i) = (⨅ (i : ι), f i, ⨅ (i : ι), g i)
                  theorem Prod.fst_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [SupSet α] [SupSet β] (f : ια × β) :
                  (iSup f).1 = ⨆ (i : ι), (f i).1
                  theorem Prod.snd_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [SupSet α] [SupSet β] (f : ια × β) :
                  (iSup f).2 = ⨆ (i : ι), (f i).2
                  theorem Prod.swap_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [SupSet α] [SupSet β] (f : ια × β) :
                  (iSup f).swap = ⨆ (i : ι), (f i).swap
                  theorem Prod.iSup_mk {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [SupSet α] [SupSet β] (f : ια) (g : ιβ) :
                  ⨆ (i : ι), (f i, g i) = (⨆ (i : ι), f i, ⨆ (i : ι), g i)
                  instance Prod.instCompleteLattice {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] :
                  Equations
                  theorem sInf_prod {α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) :
                  sInf (s ×ˢ t) = (sInf s, sInf t)
                  theorem sSup_prod {α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) :
                  sSup (s ×ˢ t) = (sSup s, sSup t)
                  theorem sup_sInf_le_iInf_sup {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} :
                  a sInf s bs, a b

                  This is a weaker version of sup_sInf_eq

                  theorem iSup_inf_le_inf_sSup {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} :
                  bs, a b a sSup s

                  This is a weaker version of inf_sSup_eq

                  theorem sInf_sup_le_iInf_sup {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} :
                  sInf s a bs, b a

                  This is a weaker version of sInf_sup_eq

                  theorem iSup_inf_le_sSup_inf {α : Type u_1} [CompleteLattice α] {a : α} {s : Set α} :
                  bs, b a sSup s a

                  This is a weaker version of sSup_inf_eq

                  theorem le_iSup_inf_iSup {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ια) (g : ια) :
                  ⨆ (i : ι), f i g i (⨆ (i : ι), f i) ⨆ (i : ι), g i
                  theorem iInf_sup_iInf_le {α : Type u_1} {ι : Sort u_4} [CompleteLattice α] (f : ια) (g : ια) :
                  (⨅ (i : ι), f i) ⨅ (i : ι), g i ⨅ (i : ι), f i g i
                  theorem disjoint_sSup_left {α : Type u_1} [CompleteLattice α] {a : Set α} {b : α} (d : Disjoint (sSup a) b) {i : α} (hi : i a) :
                  theorem disjoint_sSup_right {α : Type u_1} [CompleteLattice α] {a : Set α} {b : α} (d : Disjoint b (sSup a)) {i : α} (hi : i a) :
                  @[reducible, inline]
                  abbrev Function.Injective.completeLattice {α : Type u_1} {β : Type u_2} [Sup α] [Inf α] [SupSet α] [InfSet α] [Top α] [Bot α] [CompleteLattice β] (f : αβ) (hf : Function.Injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) (map_sSup : ∀ (s : Set α), f (sSup s) = as, f a) (map_sInf : ∀ (s : Set α), f (sInf s) = as, f a) (map_top : f = ) (map_bot : f = ) :

                  Pullback a CompleteLattice along an injection.

                  Equations
                  Instances For
                    instance ULift.supSet {α : Type u_1} [SupSet α] :
                    Equations
                    theorem ULift.down_sSup {α : Type u_1} [SupSet α] (s : Set (ULift.{v, u_1} α)) :
                    (sSup s).down = sSup (ULift.up ⁻¹' s)
                    theorem ULift.up_sSup {α : Type u_1} [SupSet α] (s : Set α) :
                    { down := sSup s } = sSup (ULift.down ⁻¹' s)
                    instance ULift.infSet {α : Type u_1} [InfSet α] :
                    Equations
                    theorem ULift.down_sInf {α : Type u_1} [InfSet α] (s : Set (ULift.{v, u_1} α)) :
                    (sInf s).down = sInf (ULift.up ⁻¹' s)
                    theorem ULift.up_sInf {α : Type u_1} [InfSet α] (s : Set α) :
                    { down := sInf s } = sInf (ULift.down ⁻¹' s)
                    theorem ULift.down_iSup {α : Type u_1} {ι : Sort u_4} [SupSet α] (f : ιULift.{v, u_1} α) :
                    (⨆ (i : ι), f i).down = ⨆ (i : ι), (f i).down
                    theorem ULift.up_iSup {α : Type u_1} {ι : Sort u_4} [SupSet α] (f : ια) :
                    { down := ⨆ (i : ι), f i } = ⨆ (i : ι), { down := f i }
                    theorem ULift.down_iInf {α : Type u_1} {ι : Sort u_4} [InfSet α] (f : ιULift.{v, u_1} α) :
                    (⨅ (i : ι), f i).down = ⨅ (i : ι), (f i).down
                    theorem ULift.up_iInf {α : Type u_1} {ι : Sort u_4} [InfSet α] (f : ια) :
                    { down := ⨅ (i : ι), f i } = ⨅ (i : ι), { down := f i }
                    Equations
                    Equations
                    • One or more equations did not get rendered due to their size.