Documentation

Mathlib.Order.CompleteLattice

Theory of complete lattices #

Main definitions #

Naming conventions #

In lemma names,

Notation #

class SupSet (α : Type u_1) :
Type u_1
  • Supremum of a set

    supₛ : Set αα

class for the supₛ operator

Instances
    class InfSet (α : Type u_1) :
    Type u_1
    • Infimum of a set

      infₛ : Set αα

    class for the infₛ operator

    Instances
      def supᵢ {α : Type u_1} [inst : SupSet α] {ι : Sort u_2} (s : ια) :
      α

      Indexed supremum

      Equations
      def infᵢ {α : Type u_1} [inst : InfSet α] {ι : Sort u_2} (s : ια) :
      α

      Indexed infimum

      Equations

      Indexed supremum.

      Equations
      • One or more equations did not get rendered due to their size.

      Unexpander for the indexed supremum notation.

      Equations
      • One or more equations did not get rendered due to their size.

      Indexed infimum.

      Equations
      • One or more equations did not get rendered due to their size.

      Unexpander for the indexed infimum notation.

      Equations
      • One or more equations did not get rendered due to their size.
      instance OrderDual.supSet (α : Type u_1) [inst : InfSet α] :
      Equations
      instance OrderDual.infSet (α : Type u_1) [inst : SupSet α] :
      Equations
      class CompleteSemilatticeSup (α : Type u_1) extends PartialOrder , SupSet :
      Type u_1
      • Any element of a set is less than the set supremum.

        le_supₛ : ∀ (s : Set α) (a : α), a sa supₛ s
      • Any upper bound is more than the set supremum.

        supₛ_le : ∀ (s : Set α) (a : α), (∀ (b : α), b sb a) → supₛ s a

      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.

      Instances
        theorem le_supₛ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α} :
        a sa supₛ s
        theorem supₛ_le {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α} :
        (∀ (b : α), b sb a) → supₛ s a
        theorem isLUB_supₛ {α : Type u_1} [inst : CompleteSemilatticeSup α] (s : Set α) :
        theorem IsLUB.supₛ_eq {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α} (h : IsLUB s a) :
        supₛ s = a
        theorem le_supₛ_of_le {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α} {b : α} (hb : b s) (h : a b) :
        theorem supₛ_le_supₛ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {t : Set α} (h : s t) :
        @[simp]
        theorem supₛ_le_iff {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α} :
        supₛ s a ∀ (b : α), b sb a
        theorem le_supₛ_iff {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α} :
        a supₛ s ∀ (b : α), b upperBounds sa b
        theorem le_supᵢ_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteSemilatticeSup α] {a : α} {s : ια} :
        a supᵢ s ∀ (b : α), (∀ (i : ι), s i b) → a b
        theorem supₛ_le_supₛ_of_forall_exists_le {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {t : Set α} (h : ∀ (x : α), x sy, y t x y) :
        theorem supₛ_singleton {α : Type u_1} [inst : CompleteSemilatticeSup α] {a : α} :
        supₛ {a} = a
        class CompleteSemilatticeInf (α : Type u_1) extends PartialOrder , InfSet :
        Type u_1
        • Any element of a set is more than the set infimum.

          infₛ_le : ∀ (s : Set α) (a : α), a sinfₛ s a
        • Any lower bound is less than the set infimum.

          le_infₛ : ∀ (s : Set α) (a : α), (∀ (b : α), b sa b) → a infₛ s

        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.

        Instances
          theorem infₛ_le {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α} :
          a sinfₛ s a
          theorem le_infₛ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α} :
          (∀ (b : α), b sa b) → a infₛ s
          theorem isGLB_infₛ {α : Type u_1} [inst : CompleteSemilatticeInf α] (s : Set α) :
          theorem IsGLB.infₛ_eq {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α} (h : IsGLB s a) :
          infₛ s = a
          theorem infₛ_le_of_le {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α} {b : α} (hb : b s) (h : b a) :
          theorem infₛ_le_infₛ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {t : Set α} (h : s t) :
          @[simp]
          theorem le_infₛ_iff {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α} :
          a infₛ s ∀ (b : α), b sa b
          theorem infₛ_le_iff {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {a : α} :
          infₛ s a ∀ (b : α), b lowerBounds sb a
          theorem infᵢ_le_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteSemilatticeInf α] {a : α} {s : ια} :
          infᵢ s a ∀ (b : α), (∀ (i : ι), b s i) → b a
          theorem infₛ_le_infₛ_of_forall_exists_le {α : Type u_1} [inst : CompleteSemilatticeInf α] {s : Set α} {t : Set α} (h : ∀ (x : α), x sy, y t y x) :
          theorem infₛ_singleton {α : Type u_1} [inst : CompleteSemilatticeInf α] {a : α} :
          infₛ {a} = a
          class CompleteLattice (α : Type u_1) extends Lattice , SupSet , InfSet , Top , Bot :
          Type u_1
          • Any element of a set is more than the set infimum.

            infₛ_le : ∀ (s : Set α) (a : α), a sinfₛ s a
          • Any lower bound is less than the set infimum.

            le_infₛ : ∀ (s : Set α) (a : α), (∀ (b : α), b sa b) → a infₛ s
          • toTop : Top α
          • toBot : Bot α
          • Any element is less than the top one.

            le_top : ∀ (x : α), x
          • Any element is more than the bottom one.

            bot_le : ∀ (x : α), x

          A complete lattice is a bounded lattice which has supᵢema and infima for every subset.

          Instances
            Equations
            • CompleteLattice.toBoundedOrder = BoundedOrder.mk
            def completeLatticeOfInf (α : Type u_1) [H1 : PartialOrder α] [H2 : InfSet α] (isGLB_infₛ : ∀ (s : Set α), IsGLB s (infₛ 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 :=
            { inf := better_inf,
              le_inf := ...,
              inf_le_right := ...,
              inf_le_left := ...
              -- don't care to fix sup, supₛ, bot, top
              ..completeLatticeOfInf my_T _ }
            
            Equations
            • One or more equations did not get rendered due to their size.

            Any CompleteSemilatticeInf is in fact a CompleteLattice.

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

            Equations
            def completeLatticeOfSup (α : Type u_1) [H1 : PartialOrder α] [H2 : SupSet α] (isLUB_supₛ : ∀ (s : Set α), IsLUB s (supₛ 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 :=
            { inf := better_inf,
              le_inf := ...,
              inf_le_right := ...,
              inf_le_left := ...
              -- don't care to fix sup, infₛ, bot, top
              ..completeLatticeOfSup my_T _ }
            
            Equations
            • One or more equations did not get rendered due to their size.

            Any CompleteSemilatticeSup is in fact a CompleteLattice.

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

            Equations
            class CompleteLinearOrder (α : Type u_1) extends CompleteLattice :
            Type u_1
            • A linear order is total.

              le_total : ∀ (a b : α), a b b a
            • In a linearly ordered type, we assume the order relations are all decidable.

              decidable_le : DecidableRel fun x x_1 => x x_1
            • In a linearly ordered type, we assume the order relations are all decidable.

              decidable_eq : DecidableEq α
            • In a linearly ordered type, we assume the order relations are all decidable.

              decidable_lt : DecidableRel fun x x_1 => x < x_1

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

            Instances
              Equations
              • CompleteLinearOrder.toLinearOrder = LinearOrder.mk (_ : ∀ (a b : α), a b b a) CompleteLinearOrder.decidable_le CompleteLinearOrder.decidable_eq CompleteLinearOrder.decidable_lt
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem toDual_supₛ {α : Type u_1} [inst : CompleteLattice α] (s : Set α) :
              OrderDual.toDual (supₛ s) = infₛ (OrderDual.ofDual ⁻¹' s)
              @[simp]
              theorem toDual_infₛ {α : Type u_1} [inst : CompleteLattice α] (s : Set α) :
              OrderDual.toDual (infₛ s) = supₛ (OrderDual.ofDual ⁻¹' s)
              @[simp]
              theorem ofDual_supₛ {α : Type u_1} [inst : CompleteLattice α] (s : Set αᵒᵈ) :
              OrderDual.ofDual (supₛ s) = infₛ (OrderDual.toDual ⁻¹' s)
              @[simp]
              theorem ofDual_infₛ {α : Type u_1} [inst : CompleteLattice α] (s : Set αᵒᵈ) :
              OrderDual.ofDual (infₛ s) = supₛ (OrderDual.toDual ⁻¹' s)
              @[simp]
              theorem toDual_supᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ια) :
              OrderDual.toDual (i, f i) = i, OrderDual.toDual (f i)
              @[simp]
              theorem toDual_infᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ια) :
              OrderDual.toDual (i, f i) = i, OrderDual.toDual (f i)
              @[simp]
              theorem ofDual_supᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ιαᵒᵈ) :
              OrderDual.ofDual (i, f i) = i, OrderDual.ofDual (f i)
              @[simp]
              theorem ofDual_infᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ιαᵒᵈ) :
              OrderDual.ofDual (i, f i) = i, OrderDual.ofDual (f i)
              theorem infₛ_le_supₛ {α : Type u_1} [inst : CompleteLattice α] {s : Set α} (hs : Set.Nonempty s) :
              theorem supₛ_union {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {t : Set α} :
              theorem infₛ_union {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {t : Set α} :
              theorem supₛ_inter_le {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {t : Set α} :
              theorem le_infₛ_inter {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {t : Set α} :
              @[simp]
              theorem supₛ_empty {α : Type u_1} [inst : CompleteLattice α] :
              @[simp]
              theorem infₛ_empty {α : Type u_1} [inst : CompleteLattice α] :
              @[simp]
              theorem supₛ_univ {α : Type u_1} [inst : CompleteLattice α] :
              supₛ Set.univ =
              @[simp]
              theorem infₛ_univ {α : Type u_1} [inst : CompleteLattice α] :
              infₛ Set.univ =
              @[simp]
              theorem supₛ_insert {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α} :
              @[simp]
              theorem infₛ_insert {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α} :
              theorem supₛ_le_supₛ_of_subset_insert_bot {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {t : Set α} (h : s insert t) :
              theorem infₛ_le_infₛ_of_subset_insert_top {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {t : Set α} (h : s insert t) :
              @[simp]
              theorem supₛ_diff_singleton_bot {α : Type u_1} [inst : CompleteLattice α] (s : Set α) :
              supₛ (s \ {}) = supₛ s
              @[simp]
              theorem infₛ_diff_singleton_top {α : Type u_1} [inst : CompleteLattice α] (s : Set α) :
              infₛ (s \ {}) = infₛ s
              theorem supₛ_pair {α : Type u_1} [inst : CompleteLattice α] {a : α} {b : α} :
              supₛ {a, b} = a b
              theorem infₛ_pair {α : Type u_1} [inst : CompleteLattice α] {a : α} {b : α} :
              infₛ {a, b} = a b
              @[simp]
              theorem supₛ_eq_bot {α : Type u_1} [inst : CompleteLattice α] {s : Set α} :
              supₛ s = ∀ (a : α), a sa =
              @[simp]
              theorem infₛ_eq_top {α : Type u_1} [inst : CompleteLattice α] {s : Set α} :
              infₛ s = ∀ (a : α), a sa =
              theorem eq_singleton_bot_of_supₛ_eq_bot_of_nonempty {α : Type u_1} [inst : CompleteLattice α] {s : Set α} (h_sup : supₛ s = ) (hne : Set.Nonempty s) :
              s = {}
              theorem supₛ_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {b : α} (h₁ : ∀ (a : α), a sa b) (h₂ : ∀ (w : α), w < ba, a s w < a) :
              supₛ 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 csupₛ_eq_of_forall_le_of_forall_lt_exists_gt for a version in conditionally complete lattices.

              theorem infₛ_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {b : α} :
              (∀ (a : α), a sb a) → (∀ (w : α), b < wa, a s a < w) → infₛ 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 cinfₛ_eq_of_forall_ge_of_forall_gt_exists_lt for a version in conditionally complete lattices.

              theorem lt_supₛ_iff {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α} {b : α} :
              b < supₛ s a, a s b < a
              theorem infₛ_lt_iff {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α} {b : α} :
              infₛ s < b a, a s a < b
              theorem supₛ_eq_top {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α} :
              supₛ s = ∀ (b : α), b < a, a s b < a
              theorem infₛ_eq_bot {α : Type u_1} [inst : CompleteLinearOrder α] {s : Set α} :
              infₛ s = ∀ (b : α), b > a, a s a < b
              theorem lt_supᵢ_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteLinearOrder α] {a : α} {f : ια} :
              a < supᵢ f i, a < f i
              theorem infᵢ_lt_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteLinearOrder α] {a : α} {f : ια} :
              infᵢ f < a i, f i < a
              theorem supₛ_range {α : Type u_1} {ι : Sort u_2} [inst : SupSet α] {f : ια} :
              theorem supₛ_eq_supᵢ' {α : Type u_1} [inst : SupSet α] (s : Set α) :
              supₛ s = a, a
              theorem supᵢ_congr {α : Type u_1} {ι : Sort u_2} [inst : SupSet α] {f : ια} {g : ια} (h : ∀ (i : ι), f i = g i) :
              (i, f i) = i, g i
              theorem Function.Surjective.supᵢ_comp {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : SupSet α] {f : ιι'} (hf : Function.Surjective f) (g : ι'α) :
              (x, g (f x)) = y, g y
              theorem Equiv.supᵢ_comp {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : SupSet α] {g : ι'α} (e : ι ι') :
              (x, g (e x)) = y, g y
              theorem Function.Surjective.supᵢ_congr {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : SupSet α] {f : ια} {g : ι'α} (h : ιι') (h1 : Function.Surjective h) (h2 : ∀ (x : ι), g (h x) = f x) :
              (x, f x) = y, g y
              theorem Equiv.supᵢ_congr {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : SupSet α] {f : ια} {g : ι'α} (e : ι ι') (h : ∀ (x : ι), g (e x) = f x) :
              (x, f x) = y, g y
              theorem supᵢ_congr_Prop {α : Type u_1} [inst : SupSet α] {p : Prop} {q : Prop} {f₁ : pα} {f₂ : qα} (pq : p q) (f : ∀ (x : q), f₁ (Iff.mpr pq x) = f₂ x) :
              supᵢ f₁ = supᵢ f₂
              theorem supᵢ_plift_up {α : Type u_2} {ι : Sort u_1} [inst : SupSet α] (f : PLift ια) :
              (i, f { down := i }) = i, f i
              theorem supᵢ_plift_down {α : Type u_1} {ι : Sort u_2} [inst : SupSet α] (f : ια) :
              (i, f i.down) = i, f i
              theorem supᵢ_range' {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SupSet α] (g : βα) (f : ιβ) :
              (b, g b) = i, g (f i)
              theorem supₛ_image' {α : Type u_2} {β : Type u_1} [inst : SupSet α] {s : Set β} {f : βα} :
              supₛ (f '' s) = a, f a
              theorem infₛ_range {α : Type u_1} {ι : Sort u_2} [inst : InfSet α] {f : ια} :
              theorem infₛ_eq_infᵢ' {α : Type u_1} [inst : InfSet α] (s : Set α) :
              infₛ s = a, a
              theorem infᵢ_congr {α : Type u_1} {ι : Sort u_2} [inst : InfSet α] {f : ια} {g : ια} (h : ∀ (i : ι), f i = g i) :
              (i, f i) = i, g i
              theorem Function.Surjective.infᵢ_comp {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : InfSet α] {f : ιι'} (hf : Function.Surjective f) (g : ι'α) :
              (x, g (f x)) = y, g y
              theorem Equiv.infᵢ_comp {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : InfSet α] {g : ι'α} (e : ι ι') :
              (x, g (e x)) = y, g y
              theorem Function.Surjective.infᵢ_congr {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : InfSet α] {f : ια} {g : ι'α} (h : ιι') (h1 : Function.Surjective h) (h2 : ∀ (x : ι), g (h x) = f x) :
              (x, f x) = y, g y
              theorem Equiv.infᵢ_congr {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_2} [inst : InfSet α] {f : ια} {g : ι'α} (e : ι ι') (h : ∀ (x : ι), g (e x) = f x) :
              (x, f x) = y, g y
              theorem infᵢ_congr_Prop {α : Type u_1} [inst : InfSet α] {p : Prop} {q : Prop} {f₁ : pα} {f₂ : qα} (pq : p q) (f : ∀ (x : q), f₁ (Iff.mpr pq x) = f₂ x) :
              infᵢ f₁ = infᵢ f₂
              theorem infᵢ_plift_up {α : Type u_2} {ι : Sort u_1} [inst : InfSet α] (f : PLift ια) :
              (i, f { down := i }) = i, f i
              theorem infᵢ_plift_down {α : Type u_1} {ι : Sort u_2} [inst : InfSet α] (f : ια) :
              (i, f i.down) = i, f i
              theorem infᵢ_range' {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : InfSet α] (g : βα) (f : ιβ) :
              (b, g b) = i, g (f i)
              theorem infₛ_image' {α : Type u_2} {β : Type u_1} [inst : InfSet α] {s : Set β} {f : βα} :
              infₛ (f '' s) = a, f a
              theorem le_supᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ια) (i : ι) :
              f i supᵢ f
              theorem infᵢ_le {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ια) (i : ι) :
              infᵢ f f i
              theorem le_supᵢ' {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ια) (i : ι) :
              f i supᵢ f
              theorem infᵢ_le' {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ια) (i : ι) :
              infᵢ f f i
              theorem isLUB_supᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} :
              IsLUB (Set.range f) (j, f j)
              theorem isGLB_infᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} :
              IsGLB (Set.range f) (j, f j)
              theorem IsLUB.supᵢ_eq {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {a : α} (h : IsLUB (Set.range f) a) :
              (j, f j) = a
              theorem IsGLB.infᵢ_eq {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {a : α} (h : IsGLB (Set.range f) a) :
              (j, f j) = a
              theorem le_supᵢ_of_le {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {a : α} (i : ι) (h : a f i) :
              theorem infᵢ_le_of_le {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {a : α} (i : ι) (h : f i a) :
              theorem le_supᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : CompleteLattice α] {f : (i : ι) → κ iα} (i : ι) (j : κ i) :
              f i j i, j, f i j
              theorem infᵢ₂_le {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : CompleteLattice α] {f : (i : ι) → κ iα} (i : ι) (j : κ i) :
              (i, j, f i j) f i j
              theorem le_supᵢ₂_of_le {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ iα} (i : ι) (j : κ i) (h : a f i j) :
              a i, j, f i j
              theorem infᵢ₂_le_of_le {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ iα} (i : ι) (j : κ i) (h : f i j a) :
              (i, j, f i j) a
              theorem supᵢ_le {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {a : α} (h : ∀ (i : ι), f i a) :
              theorem le_infᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {a : α} (h : ∀ (i : ι), a f i) :
              theorem supᵢ₂_le {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ iα} (h : ∀ (i : ι) (j : κ i), f i j a) :
              (i, j, f i j) a
              theorem le_infᵢ₂ {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ iα} (h : ∀ (i : ι) (j : κ i), a f i j) :
              a i, j, f i j
              theorem supᵢ₂_le_supᵢ {α : Type u_2} {ι : Sort u_3} [inst : CompleteLattice α] (κ : ιSort u_1) (f : ια) :
              (i, _j, f i) i, f i
              theorem infᵢ_le_infᵢ₂ {α : Type u_2} {ι : Sort u_3} [inst : CompleteLattice α] (κ : ιSort u_1) (f : ια) :
              (i, f i) i, _j, f i
              theorem supᵢ_mono {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {g : ια} (h : ∀ (i : ι), f i g i) :
              theorem infᵢ_mono {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {g : ια} (h : ∀ (i : ι), f i g i) :
              theorem supᵢ₂_mono {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : CompleteLattice α] {f : (i : ι) → κ iα} {g : (i : ι) → κ iα} (h : ∀ (i : ι) (j : κ i), f i j g i j) :
              (i, j, f i j) i, j, g i j
              theorem infᵢ₂_mono {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : CompleteLattice α] {f : (i : ι) → κ iα} {g : (i : ι) → κ iα} (h : ∀ (i : ι) (j : κ i), f i j g i j) :
              (i, j, f i j) i, j, g i j
              theorem supᵢ_mono' {α : Type u_2} {ι : Sort u_3} {ι' : Sort u_1} [inst : CompleteLattice α] {f : ια} {g : ι'α} (h : ∀ (i : ι), i', f i g i') :
              theorem infᵢ_mono' {α : Type u_2} {ι : Sort u_1} {ι' : Sort u_3} [inst : CompleteLattice α] {f : ια} {g : ι'α} (h : ∀ (i' : ι'), i, f i g i') :
              theorem supᵢ₂_mono' {α : Type u_3} {ι : Sort u_4} {ι' : Sort u_1} {κ : ιSort u_5} {κ' : ι'Sort u_2} [inst : CompleteLattice α] {f : (i : ι) → κ iα} {g : (i' : ι') → κ' i'α} (h : ∀ (i : ι) (j : κ i), i' j', f i j g i' j') :
              (i, j, f i j) i, j, g i j
              theorem infᵢ₂_mono' {α : Type u_3} {ι : Sort u_1} {ι' : Sort u_4} {κ : ιSort u_2} {κ' : ι'Sort u_5} [inst : CompleteLattice α] {f : (i : ι) → κ iα} {g : (i' : ι') → κ' i'α} (h : ∀ (i : ι') (j : κ' i), i' j', f i' j' g i j) :
              (i, j, f i j) i, j, g i j
              theorem supᵢ_const_mono {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : CompleteLattice α] {a : α} (h : ιι') :
              (_i, a) _j, a
              theorem infᵢ_const_mono {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : CompleteLattice α] {a : α} (h : ι'ι) :
              (_i, a) _j, a
              theorem supᵢ_infᵢ_le_infᵢ_supᵢ {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : CompleteLattice α] (f : ιι'α) :
              (i, j, f i j) j, i, f i j
              theorem bsupᵢ_mono {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {p : ιProp} {q : ιProp} (hpq : (i : ι) → p iq i) :
              (i, _h, f i) i, _h, f i
              theorem binfᵢ_mono {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {p : ιProp} {q : ιProp} (hpq : (i : ι) → p iq i) :
              (i, _h, f i) i, _h, f i
              @[simp]
              theorem supᵢ_le_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {a : α} :
              supᵢ f a ∀ (i : ι), f i a
              @[simp]
              theorem le_infᵢ_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {a : α} :
              a infᵢ f ∀ (i : ι), a f i
              theorem supᵢ₂_le_iff {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ iα} :
              (i, j, f i j) a ∀ (i : ι) (j : κ i), f i j a
              theorem le_infᵢ₂_iff {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : CompleteLattice α] {a : α} {f : (i : ι) → κ iα} :
              (a i, j, f i j) ∀ (i : ι) (j : κ i), a f i j
              theorem supᵢ_lt_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {a : α} :
              supᵢ f < a b, b < a ∀ (i : ι), f i b
              theorem lt_infᵢ_iff {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {a : α} :
              a < infᵢ f b, a < b ∀ (i : ι), b f i
              theorem supₛ_eq_supᵢ {α : Type u_1} [inst : CompleteLattice α] {s : Set α} :
              supₛ s = a, h, a
              theorem infₛ_eq_infᵢ {α : Type u_1} [inst : CompleteLattice α] {s : Set α} :
              infₛ s = a, h, a
              theorem Monotone.le_map_supᵢ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] {s : ια} [inst : CompleteLattice β] {f : αβ} (hf : Monotone f) :
              (i, f (s i)) f (supᵢ s)
              theorem Antitone.le_map_infᵢ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] {s : ια} [inst : CompleteLattice β] {f : αβ} (hf : Antitone f) :
              (i, f (s i)) f (infᵢ s)
              theorem Monotone.le_map_supᵢ₂ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : αβ} (hf : Monotone f) (s : (i : ι) → κ iα) :
              (i, j, f (s i j)) f (i, j, s i j)
              theorem Antitone.le_map_infᵢ₂ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : αβ} (hf : Antitone f) (s : (i : ι) → κ iα) :
              (i, j, f (s i j)) f (i, j, s i j)
              theorem Monotone.le_map_supₛ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] [inst : CompleteLattice β] {s : Set α} {f : αβ} (hf : Monotone f) :
              (a, h, f a) f (supₛ s)
              theorem Antitone.le_map_infₛ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] [inst : CompleteLattice β] {s : Set α} {f : αβ} (hf : Antitone f) :
              (a, h, f a) f (infₛ s)
              theorem OrderIso.map_supᵢ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] [inst : CompleteLattice β] (f : α ≃o β) (x : ια) :
              (RelIso.toRelEmbedding f).toEmbedding (i, x i) = i, (RelIso.toRelEmbedding f).toEmbedding (x i)
              theorem OrderIso.map_infᵢ {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] [inst : CompleteLattice β] (f : α ≃o β) (x : ια) :
              (RelIso.toRelEmbedding f).toEmbedding (i, x i) = i, (RelIso.toRelEmbedding f).toEmbedding (x i)
              theorem OrderIso.map_supₛ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] [inst : CompleteLattice β] (f : α ≃o β) (s : Set α) :
              (RelIso.toRelEmbedding f).toEmbedding (supₛ s) = a, h, (RelIso.toRelEmbedding f).toEmbedding a
              theorem OrderIso.map_infₛ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] [inst : CompleteLattice β] (f : α ≃o β) (s : Set α) :
              (RelIso.toRelEmbedding f).toEmbedding (infₛ s) = a, h, (RelIso.toRelEmbedding f).toEmbedding a
              theorem supᵢ_comp_le {α : Type u_2} {ι : Sort u_3} [inst : CompleteLattice α] {ι' : Sort u_1} (f : ι'α) (g : ιι') :
              (x, f (g x)) y, f y
              theorem le_infᵢ_comp {α : Type u_2} {ι : Sort u_3} [inst : CompleteLattice α] {ι' : Sort u_1} (f : ι'α) (g : ιι') :
              (y, f y) x, f (g x)
              theorem Monotone.supᵢ_comp_eq {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] [inst : Preorder β] {f : βα} (hf : Monotone f) {s : ιβ} (hs : ∀ (x : β), i, x s i) :
              (x, f (s x)) = y, f y
              theorem Monotone.infᵢ_comp_eq {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] [inst : Preorder β] {f : βα} (hf : Monotone f) {s : ιβ} (hs : ∀ (x : β), i, s i x) :
              (x, f (s x)) = y, f y
              theorem Antitone.map_supᵢ_le {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] {s : ια} [inst : CompleteLattice β] {f : αβ} (hf : Antitone f) :
              f (supᵢ s) i, f (s i)
              theorem Monotone.map_infᵢ_le {α : Type u_2} {β : Type u_1} {ι : Sort u_3} [inst : CompleteLattice α] {s : ια} [inst : CompleteLattice β] {f : αβ} (hf : Monotone f) :
              f (infᵢ s) i, f (s i)
              theorem Antitone.map_supᵢ₂_le {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : αβ} (hf : Antitone f) (s : (i : ι) → κ iα) :
              f (i, j, s i j) i, j, f (s i j)
              theorem Monotone.map_infᵢ₂_le {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} [inst : CompleteLattice α] [inst : CompleteLattice β] {f : αβ} (hf : Monotone f) (s : (i : ι) → κ iα) :
              f (i, j, s i j) i, j, f (s i j)
              theorem Antitone.map_supₛ_le {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] [inst : CompleteLattice β] {s : Set α} {f : αβ} (hf : Antitone f) :
              f (supₛ s) a, h, f a
              theorem Monotone.map_infₛ_le {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] [inst : CompleteLattice β] {s : Set α} {f : αβ} (hf : Monotone f) :
              f (infₛ s) a, h, f a
              theorem supᵢ_const_le {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {a : α} :
              (_i, a) a
              theorem le_infᵢ_const {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {a : α} :
              a _i, a
              theorem supᵢ_const {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {a : α} [inst : Nonempty ι] :
              (_b, a) = a
              theorem infᵢ_const {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {a : α} [inst : Nonempty ι] :
              (_b, a) = a
              @[simp]
              theorem supᵢ_bot {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] :
              (_i, ) =
              @[simp]
              theorem infᵢ_top {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] :
              (_i, ) =
              @[simp]
              theorem supᵢ_eq_bot {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {s : ια} :
              supᵢ s = ∀ (i : ι), s i =
              @[simp]
              theorem infᵢ_eq_top {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {s : ια} :
              infᵢ s = ∀ (i : ι), s i =
              theorem supᵢ₂_eq_bot {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : CompleteLattice α] {f : (i : ι) → κ iα} :
              (i, j, f i j) = ∀ (i : ι) (j : κ i), f i j =
              theorem infᵢ₂_eq_top {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : CompleteLattice α] {f : (i : ι) → κ iα} :
              (i, j, f i j) = ∀ (i : ι) (j : κ i), f i j =
              @[simp]
              theorem supᵢ_pos {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {f : pα} (hp : p) :
              (h, f h) = f hp
              @[simp]
              theorem infᵢ_pos {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {f : pα} (hp : p) :
              (h, f h) = f hp
              @[simp]
              theorem supᵢ_neg {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {f : pα} (hp : ¬p) :
              (h, f h) =
              @[simp]
              theorem infᵢ_neg {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {f : pα} (hp : ¬p) :
              (h, f h) =
              theorem supᵢ_eq_of_forall_le_of_forall_lt_exists_gt {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {b : α} {f : ια} (h₁ : ∀ (i : ι), f i b) (h₂ : ∀ (w : α), w < bi, 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. See csupᵢ_eq_of_forall_le_of_forall_lt_exists_gt for a version in conditionally complete lattices.

              theorem infᵢ_eq_of_forall_ge_of_forall_gt_exists_lt {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {b : α} :
              (∀ (i : ι), b f i) → (∀ (w : α), b < wi, 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 cinfᵢ_eq_of_forall_ge_of_forall_gt_exists_lt for a version in conditionally complete lattices.

              theorem supᵢ_eq_dif {α : Type u_1} [inst : CompleteLattice α] {p : Prop} [inst : Decidable p] (a : pα) :
              (h, a h) = if h : p then a h else
              theorem supᵢ_eq_if {α : Type u_1} [inst : CompleteLattice α] {p : Prop} [inst : Decidable p] (a : α) :
              (_h, a) = if p then a else
              theorem infᵢ_eq_dif {α : Type u_1} [inst : CompleteLattice α] {p : Prop} [inst : Decidable p] (a : pα) :
              (h, a h) = if h : p then a h else
              theorem infᵢ_eq_if {α : Type u_1} [inst : CompleteLattice α] {p : Prop} [inst : Decidable p] (a : α) :
              (_h, a) = if p then a else
              theorem supᵢ_comm {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : CompleteLattice α] {f : ιι'α} :
              (i, j, f i j) = j, i, f i j
              theorem infᵢ_comm {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : CompleteLattice α] {f : ιι'α} :
              (i, j, f i j) = j, i, f i j
              theorem supᵢ₂_comm {α : Type u_5} [inst : CompleteLattice α] {ι₁ : Sort u_1} {ι₂ : Sort u_2} {κ₁ : ι₁Sort u_3} {κ₂ : ι₂Sort u_4} (f : (i₁ : ι₁) → κ₁ i₁(i₂ : ι₂) → κ₂ i₂α) :
              (i₁, j₁, i₂, j₂, f i₁ j₁ i₂ j₂) = i₂, j₂, i₁, j₁, f i₁ j₁ i₂ j₂
              theorem infᵢ₂_comm {α : Type u_5} [inst : CompleteLattice α] {ι₁ : Sort u_1} {ι₂ : Sort u_2} {κ₁ : ι₁Sort u_3} {κ₂ : ι₂Sort u_4} (f : (i₁ : ι₁) → κ₁ i₁(i₂ : ι₂) → κ₂ i₂α) :
              (i₁, j₁, i₂, j₂, f i₁ j₁ i₂ j₂) = i₂, j₂, i₁, j₁, f i₁ j₁ i₂ j₂
              @[simp]
              theorem supᵢ_supᵢ_eq_left {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {b : β} {f : (x : β) → x = bα} :
              (x, h, f x h) = f b (_ : b = b)
              @[simp]
              theorem infᵢ_infᵢ_eq_left {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {b : β} {f : (x : β) → x = bα} :
              (x, h, f x h) = f b (_ : b = b)
              @[simp]
              theorem supᵢ_supᵢ_eq_right {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {b : β} {f : (x : β) → b = xα} :
              (x, h, f x h) = f b (_ : b = b)
              @[simp]
              theorem infᵢ_infᵢ_eq_right {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {b : β} {f : (x : β) → b = xα} :
              (x, h, f x h) = f b (_ : b = b)
              theorem supᵢ_subtype {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ιProp} {f : Subtype pα} :
              supᵢ f = i, h, f { val := i, property := h }
              theorem infᵢ_subtype {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ιProp} {f : Subtype pα} :
              infᵢ f = i, h, f { val := i, property := h }
              theorem supᵢ_subtype' {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {p : ιProp} {f : (i : ι) → p iα} :
              (i, h, f i h) = x, f (x) x.property
              theorem infᵢ_subtype' {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {p : ιProp} {f : (i : ι) → p iα} :
              (i, h, f i h) = x, f (x) x.property
              theorem supᵢ_subtype'' {α : Type u_2} [inst : CompleteLattice α] {ι : Type u_1} (s : Set ι) (f : ια) :
              (i, f i) = t, _H, f t
              theorem infᵢ_subtype'' {α : Type u_2} [inst : CompleteLattice α] {ι : Type u_1} (s : Set ι) (f : ια) :
              (i, f i) = t, _H, f t
              theorem bsupᵢ_const {α : Type u_2} [inst : CompleteLattice α] {ι : Type u_1} {a : α} {s : Set ι} (hs : Set.Nonempty s) :
              (i, h, a) = a
              theorem binfᵢ_const {α : Type u_2} [inst : CompleteLattice α] {ι : Type u_1} {a : α} {s : Set ι} (hs : Set.Nonempty s) :
              (i, h, a) = a
              theorem supᵢ_sup_eq {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {g : ια} :
              (x, f x g x) = (x, f x) x, g x
              theorem infᵢ_inf_eq {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] {f : ια} {g : ια} :
              (x, f x g x) = (x, f x) x, g x
              theorem supᵢ_sup {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] [inst : Nonempty ι] {f : ια} {a : α} :
              (x, f x) a = x, f x a
              theorem infᵢ_inf {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] [inst : Nonempty ι] {f : ια} {a : α} :
              (x, f x) a = x, f x a
              theorem sup_supᵢ {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] [inst : Nonempty ι] {f : ια} {a : α} :
              (a x, f x) = x, a f x
              theorem inf_infᵢ {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] [inst : Nonempty ι] {f : ια} {a : α} :
              (a x, f x) = x, a f x
              theorem bsupᵢ_sup {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ιProp} {f : (i : ι) → p iα} {a : α} (h : i, p i) :
              (i, h, f i h) a = i, h, f i h a
              theorem sup_bsupᵢ {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ιProp} {f : (i : ι) → p iα} {a : α} (h : i, p i) :
              (a i, h, f i h) = i, h, a f i h
              theorem binfᵢ_inf {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ιProp} {f : (i : ι) → p iα} {a : α} (h : i, p i) :
              (i, h, f i h) a = i, h, f i h a
              theorem inf_binfᵢ {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ιProp} {f : (i : ι) → p iα} {a : α} (h : i, p i) :
              (a i, h, f i h) = i, h, a f i h

              supᵢ and infᵢ under Prop #

              theorem supᵢ_false {α : Type u_1} [inst : CompleteLattice α] {s : Falseα} :
              theorem infᵢ_false {α : Type u_1} [inst : CompleteLattice α] {s : Falseα} :
              theorem supᵢ_true {α : Type u_1} [inst : CompleteLattice α] {s : Trueα} :
              theorem infᵢ_true {α : Type u_1} [inst : CompleteLattice α] {s : Trueα} :
              @[simp]
              theorem supᵢ_exists {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ιProp} {f : Exists pα} :
              (x, f x) = i, h, f (_ : Exists p)
              @[simp]
              theorem infᵢ_exists {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {p : ιProp} {f : Exists pα} :
              (x, f x) = i, h, f (_ : Exists p)
              theorem supᵢ_and {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {q : Prop} {s : p qα} :
              supᵢ s = h₁, h₂, s (_ : p q)
              theorem infᵢ_and {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {q : Prop} {s : p qα} :
              infᵢ s = h₁, h₂, s (_ : p q)
              theorem supᵢ_and' {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {q : Prop} {s : pqα} :
              (h₁, h₂, s h₁ h₂) = h, s h.left h.right

              The symmetric case of supᵢ_and, useful for rewriting into a supremum over a conjunction

              theorem infᵢ_and' {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {q : Prop} {s : pqα} :
              (h₁, h₂, s h₁ h₂) = h, s h.left h.right

              The symmetric case of infᵢ_and, useful for rewriting into a infimum over a conjunction

              theorem supᵢ_or {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {q : Prop} {s : p qα} :
              (x, s x) = (i, s (_ : p q)) j, s (_ : p q)
              theorem infᵢ_or {α : Type u_1} [inst : CompleteLattice α] {p : Prop} {q : Prop} {s : p qα} :
              (x, s x) = (i, s (_ : p q)) j, s (_ : p q)
              theorem supᵢ_dite {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (p : ιProp) [inst : 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, f i h) i, h, g i h
              theorem infᵢ_dite {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (p : ιProp) [inst : 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, f i h) i, h, g i h
              theorem supᵢ_ite {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (p : ιProp) [inst : DecidablePred p] (f : ια) (g : ια) :
              (i, if p i then f i else g i) = (i, _h, f i) i, _h, g i
              theorem infᵢ_ite {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (p : ιProp) [inst : DecidablePred p] (f : ια) (g : ια) :
              (i, if p i then f i else g i) = (i, _h, f i) i, _h, g i
              theorem supᵢ_range {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : CompleteLattice α] {g : βα} {f : ιβ} :
              (b, h, g b) = i, g (f i)
              theorem infᵢ_range {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : CompleteLattice α] {g : βα} {f : ιβ} :
              (b, h, g b) = i, g (f i)
              theorem supₛ_image {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {s : Set β} {f : βα} :
              supₛ (f '' s) = a, h, f a
              theorem infₛ_image {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {s : Set β} {f : βα} :
              infₛ (f '' s) = a, h, f a
              theorem supᵢ_emptyset {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : βα} :
              (x, h, f x) =
              theorem infᵢ_emptyset {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : βα} :
              (x, h, f x) =
              theorem supᵢ_univ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : βα} :
              (x, h, f x) = x, f x
              theorem infᵢ_univ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : βα} :
              (x, h, f x) = x, f x
              theorem supᵢ_union {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {f : βα} {s : Set β} {t : Set β} :
              (x, h, f x) = (x, h, f x) x, h, f x
              theorem infᵢ_union {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {f : βα} {s : Set β} {t : Set β} :
              (x, h, f x) = (x, h, f x) x, h, f x
              theorem supᵢ_split {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : βα) (p : βProp) :
              (i, f i) = (i, _h, f i) i, _h, f i
              theorem infᵢ_split {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : βα) (p : βProp) :
              (i, f i) = (i, _h, f i) i, _h, f i
              theorem supᵢ_split_single {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : βα) (i₀ : β) :
              (i, f i) = f i₀ i, _h, f i
              theorem infᵢ_split_single {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : βα) (i₀ : β) :
              (i, f i) = f i₀ i, _h, f i
              theorem supᵢ_le_supᵢ_of_subset {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {f : βα} {s : Set β} {t : Set β} :
              s t(x, h, f x) x, h, f x
              theorem infᵢ_le_infᵢ_of_subset {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {f : βα} {s : Set β} {t : Set β} :
              s t(x, h, f x) x, h, f x
              theorem supᵢ_insert {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {f : βα} {s : Set β} {b : β} :
              (x, h, f x) = f b x, h, f x
              theorem infᵢ_insert {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {f : βα} {s : Set β} {b : β} :
              (x, h, f x) = f b x, h, f x
              theorem supᵢ_singleton {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : βα} {b : β} :
              (x, h, f x) = f b
              theorem infᵢ_singleton {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : βα} {b : β} :
              (x, h, f x) = f b
              theorem supᵢ_pair {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : βα} {a : β} {b : β} :
              (x, h, f x) = f a f b
              theorem infᵢ_pair {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : βα} {a : β} {b : β} :
              (x, h, f x) = f a f b
              theorem supᵢ_image {α : Type u_3} {β : Type u_2} [inst : CompleteLattice α] {γ : Type u_1} {f : βγ} {g : γα} {t : Set β} :
              (c, h, g c) = b, h, g (f b)
              theorem infᵢ_image {α : Type u_3} {β : Type u_2} [inst : CompleteLattice α] {γ : Type u_1} {f : βγ} {g : γα} {t : Set β} :
              (c, h, g c) = b, h, g (f b)
              theorem supᵢ_extend_bot {α : Type u_3} {β : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {e : ιβ} (he : Function.Injective e) (f : ια) :
              (j, Function.extend e f j) = i, f i
              theorem infᵢ_extend_top {α : Type u_3} {β : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] {e : ιβ} (he : Function.Injective e) (f : ια) :
              (j, Function.extend e f j) = infᵢ f

              supᵢ and infᵢ under Type #

              theorem supᵢ_of_empty' {α : Type u_1} {ι : Sort u_2} [inst : SupSet α] [inst : IsEmpty ι] (f : ια) :
              theorem infᵢ_of_empty' {α : Type u_1} {ι : Sort u_2} [inst : InfSet α] [inst : IsEmpty ι] (f : ια) :
              theorem supᵢ_of_empty {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] [inst : IsEmpty ι] (f : ια) :
              theorem infᵢ_of_empty {α : Type u_2} {ι : Sort u_1} [inst : CompleteLattice α] [inst : IsEmpty ι] (f : ια) :
              theorem supᵢ_bool_eq {α : Type u_1} [inst : CompleteLattice α] {f : Boolα} :
              (b, f b) = f true f false
              theorem infᵢ_bool_eq {α : Type u_1} [inst : CompleteLattice α] {f : Boolα} :
              (b, f b) = f true f false
              theorem sup_eq_supᵢ {α : Type u_1} [inst : CompleteLattice α] (x : α) (y : α) :
              x y = b, bif b then x else y
              theorem inf_eq_infᵢ {α : Type u_1} [inst : CompleteLattice α] (x : α) (y : α) :
              x y = b, bif b then x else y
              theorem isGLB_binfᵢ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {s : Set β} {f : βα} :
              IsGLB (f '' s) (x, h, f x)
              theorem isLUB_bsupᵢ {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] {s : Set β} {f : βα} :
              IsLUB (f '' s) (x, h, f x)
              theorem supᵢ_sigma {α : Type u_3} {β : Type u_2} [inst : CompleteLattice α] {p : βType u_1} {f : Sigma pα} :
              (x, f x) = i, j, f { fst := i, snd := j }
              theorem infᵢ_sigma {α : Type u_3} {β : Type u_2} [inst : CompleteLattice α] {p : βType u_1} {f : Sigma pα} :
              (x, f x) = i, j, f { fst := i, snd := j }
              theorem supᵢ_prod {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : β × γα} :
              (x, f x) = i, j, f (i, j)
              theorem infᵢ_prod {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : β × γα} :
              (x, f x) = i, j, f (i, j)
              theorem bsupᵢ_prod {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : β × γα} {s : Set β} {t : Set γ} :
              (x, h, f x) = a, h, b, h, f (a, b)
              theorem binfᵢ_prod {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : β × γα} {s : Set β} {t : Set γ} :
              (x, h, f x) = a, h, b, h, f (a, b)
              theorem supᵢ_sum {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : β γα} :
              (x, f x) = (i, f (Sum.inl i)) j, f (Sum.inr j)
              theorem infᵢ_sum {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : β γα} :
              (x, f x) = (i, f (Sum.inl i)) j, f (Sum.inr j)
              theorem supᵢ_option {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] (f : Option βα) :
              (o, f o) = f none b, f (some b)
              theorem infᵢ_option {α : Type u_2} {β : Type u_1} [inst : CompleteLattice α] (f : Option βα) :
              (o, f o) = f none b, f (some b)
              theorem supᵢ_option_elim {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (a : α) (f : βα) :
              (o, Option.elim o a f) = a b, f b

              A version of supᵢ_option useful for rewriting right-to-left.

              theorem infᵢ_option_elim {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (a : α) (f : βα) :
              (o, Option.elim o a f) = a b, f b

              A version of infᵢ_option useful for rewriting right-to-left.

              theorem supᵢ_ne_bot_subtype {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (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 infᵢ_ne_top_subtype {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (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 supₛ_image2 {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : βγα} {s : Set β} {t : Set γ} :
              supₛ (Set.image2 f s t) = a, h, b, h, f a b
              theorem infₛ_image2 {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : CompleteLattice α] {f : βγα} {s : Set β} {t : Set γ} :
              infₛ (Set.image2 f s t) = a, h, b, h, f a b

              supᵢ and infᵢ under #

              theorem supᵢ_ge_eq_supᵢ_nat_add {α : Type u_1} [inst : CompleteLattice α] (u : α) (n : ) :
              (i, h, u i) = i, u (i + n)
              theorem infᵢ_ge_eq_infᵢ_nat_add {α : Type u_1} [inst : CompleteLattice α] (u : α) (n : ) :
              (i, h, u i) = i, u (i + n)
              theorem Monotone.supᵢ_nat_add {α : Type u_1} [inst : CompleteLattice α] {f : α} (hf : Monotone f) (k : ) :
              (n, f (n + k)) = n, f n
              theorem Antitone.infᵢ_nat_add {α : Type u_1} [inst : CompleteLattice α] {f : α} (hf : Antitone f) (k : ) :
              (n, f (n + k)) = n, f n
              theorem supᵢ_infᵢ_ge_nat_add {α : Type u_1} [inst : CompleteLattice α] (f : α) (k : ) :
              (n, i, h, f (i + k)) = n, i, h, f i
              theorem infᵢ_supᵢ_ge_nat_add {α : Type u_1} [inst : CompleteLattice α] (f : α) (k : ) :
              (n, i, h, f (i + k)) = n, i, h, f i
              theorem sup_supᵢ_nat_succ {α : Type u_1} [inst : CompleteLattice α] (u : α) :
              (u 0 i, u (i + 1)) = i, u i
              theorem inf_infᵢ_nat_succ {α : Type u_1} [inst : CompleteLattice α] (u : α) :
              (u 0 i, u (i + 1)) = i, u i
              theorem infᵢ_nat_gt_zero_eq {α : Type u_1} [inst : CompleteLattice α] (f : α) :
              (i, h, f i) = i, f (i + 1)
              theorem supᵢ_nat_gt_zero_eq {α : Type u_1} [inst : CompleteLattice α] (f : α) :
              (i, h, f i) = i, f (i + 1)
              theorem supᵢ_eq_top {α : Type u_1} {ι : Sort u_2} [inst : CompleteLinearOrder α] (f : ια) :
              supᵢ f = ∀ (b : α), b < i, b < f i
              theorem infᵢ_eq_bot {α : Type u_1} {ι : Sort u_2} [inst : CompleteLinearOrder α] (f : ια) :
              infᵢ f = ∀ (b : α), b > i, f i < b

              Instances #

              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem supₛ_Prop_eq {s : Set Prop} :
              supₛ s = p, p s p
              @[simp]
              theorem infₛ_Prop_eq {s : Set Prop} :
              infₛ s = ∀ (p : Prop), p sp
              @[simp]
              theorem supᵢ_Prop_eq {ι : Sort u_1} {p : ιProp} :
              (i, p i) = i, p i
              @[simp]
              theorem infᵢ_Prop_eq {ι : Sort u_1} {p : ιProp} :
              (i, p i) = ((i : ι) → p i)
              instance Pi.supSet {α : Type u_1} {β : αType u_2} [inst : (i : α) → SupSet (β i)] :
              SupSet ((i : α) → β i)
              Equations
              • Pi.supSet = { supₛ := fun s i => f, f i }
              instance Pi.infSet {α : Type u_1} {β : αType u_2} [inst : (i : α) → InfSet (β i)] :
              InfSet ((i : α) → β i)
              Equations
              • Pi.infSet = { infₛ := fun s i => f, f i }
              instance Pi.completeLattice {α : Type u_1} {β : αType u_2} [inst : (i : α) → CompleteLattice (β i)] :
              CompleteLattice ((i : α) → β i)
              Equations
              • One or more equations did not get rendered due to their size.
              theorem supₛ_apply {α : Type u_1} {β : αType u_2} [inst : (i : α) → SupSet (β i)] {s : Set ((a : α) → β a)} {a : α} :
              supₛ ((a : α) → β a) Pi.supSet s a = f, f a
              theorem infₛ_apply {α : Type u_1} {β : αType u_2} [inst : (i : α) → InfSet (β i)] {s : Set ((a : α) → β a)} {a : α} :
              infₛ ((a : α) → β a) Pi.infSet s a = f, f a
              @[simp]
              theorem supᵢ_apply {α : Type u_1} {β : αType u_2} {ι : Sort u_3} [inst : (i : α) → SupSet (β i)] {f : ι(a : α) → β a} {a : α} :
              supᵢ ((a : α) → β a) Pi.supSet ι (fun i => f i) a = i, f i a
              @[simp]
              theorem infᵢ_apply {α : Type u_1} {β : αType u_2} {ι : Sort u_3} [inst : (i : α) → InfSet (β i)] {f : ι(a : α) → β a} {a : α} :
              infᵢ ((a : α) → β a) Pi.infSet ι (fun i => f i) a = i, f i a
              theorem unary_relation_supₛ_iff {α : Type u_1} (s : Set (αProp)) {a : α} :
              supₛ s a r, r s r a
              theorem unary_relation_infₛ_iff {α : Type u_1} (s : Set (αProp)) {a : α} :
              infₛ s a (r : αProp) → r sr a
              theorem binary_relation_supₛ_iff {α : Type u_1} {β : Type u_2} (s : Set (αβProp)) {a : α} {b : β} :
              supₛ s a b r, r s r a b
              theorem binary_relation_infₛ_iff {α : Type u_1} {β : Type u_2} (s : Set (αβProp)) {a : α} {b : β} :
              infₛ s a b (r : αβProp) → r sr a b
              theorem monotone_supₛ_of_monotone {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : CompleteLattice β] {s : Set (αβ)} (m_s : ∀ (f : αβ), f sMonotone f) :
              theorem monotone_infₛ_of_monotone {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : CompleteLattice β] {s : Set (αβ)} (m_s : ∀ (f : αβ), f sMonotone f) :
              instance Prod.supSet (α : Type u_1) (β : Type u_2) [inst : SupSet α] [inst : SupSet β] :
              SupSet (α × β)
              Equations
              instance Prod.infSet (α : Type u_1) (β : Type u_2) [inst : InfSet α] [inst : InfSet β] :
              InfSet (α × β)
              Equations
              theorem Prod.fst_infₛ {α : Type u_1} {β : Type u_2} [inst : InfSet α] [inst : InfSet β] (s : Set (α × β)) :
              (infₛ s).fst = infₛ (Prod.fst '' s)
              theorem Prod.snd_infₛ {α : Type u_1} {β : Type u_2} [inst : InfSet α] [inst : InfSet β] (s : Set (α × β)) :
              (infₛ s).snd = infₛ (Prod.snd '' s)
              theorem Prod.swap_infₛ {α : Type u_1} {β : Type u_2} [inst : InfSet α] [inst : InfSet β] (s : Set (α × β)) :
              Prod.swap (infₛ s) = infₛ (Prod.swap '' s)
              theorem Prod.fst_supₛ {α : Type u_1} {β : Type u_2} [inst : SupSet α] [inst : SupSet β] (s : Set (α × β)) :
              (supₛ s).fst = supₛ (Prod.fst '' s)
              theorem Prod.snd_supₛ {α : Type u_1} {β : Type u_2} [inst : SupSet α] [inst : SupSet β] (s : Set (α × β)) :
              (supₛ s).snd = supₛ (Prod.snd '' s)
              theorem Prod.swap_supₛ {α : Type u_1} {β : Type u_2} [inst : SupSet α] [inst : SupSet β] (s : Set (α × β)) :
              Prod.swap (supₛ s) = supₛ (Prod.swap '' s)
              theorem Prod.fst_infᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : InfSet α] [inst : InfSet β] (f : ια × β) :
              (infᵢ f).fst = i, (f i).fst
              theorem Prod.snd_infᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : InfSet α] [inst : InfSet β] (f : ια × β) :
              (infᵢ f).snd = i, (f i).snd
              theorem Prod.swap_infᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : InfSet α] [inst : InfSet β] (f : ια × β) :
              Prod.swap (infᵢ f) = i, Prod.swap (f i)
              theorem Prod.infᵢ_mk {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : InfSet α] [inst : InfSet β] (f : ια) (g : ιβ) :
              (i, (f i, g i)) = (i, f i, i, g i)
              theorem Prod.fst_supᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SupSet α] [inst : SupSet β] (f : ια × β) :
              (supᵢ f).fst = i, (f i).fst
              theorem Prod.snd_supᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SupSet α] [inst : SupSet β] (f : ια × β) :
              (supᵢ f).snd = i, (f i).snd
              theorem Prod.swap_supᵢ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SupSet α] [inst : SupSet β] (f : ια × β) :
              Prod.swap (supᵢ f) = i, Prod.swap (f i)
              theorem Prod.supᵢ_mk {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [inst : SupSet α] [inst : SupSet β] (f : ια) (g : ιβ) :
              (i, (f i, g i)) = (i, f i, i, g i)
              instance Prod.completeLattice (α : Type u_1) (β : Type u_2) [inst : CompleteLattice α] [inst : CompleteLattice β] :
              Equations
              • One or more equations did not get rendered due to their size.
              theorem infₛ_prod {α : Type u_1} {β : Type u_2} [inst : InfSet α] [inst : InfSet β] {s : Set α} {t : Set β} (hs : Set.Nonempty s) (ht : Set.Nonempty t) :
              infₛ (s ×ˢ t) = (infₛ s, infₛ t)
              theorem supₛ_prod {α : Type u_1} {β : Type u_2} [inst : SupSet α] [inst : SupSet β] {s : Set α} {t : Set β} (hs : Set.Nonempty s) (ht : Set.Nonempty t) :
              supₛ (s ×ˢ t) = (supₛ s, supₛ t)
              theorem sup_infₛ_le_infᵢ_sup {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α} :
              a infₛ s b, h, a b

              This is a weaker version of sup_infₛ_eq

              theorem supᵢ_inf_le_inf_supₛ {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α} :
              (b, h, a b) a supₛ s

              This is a weaker version of inf_supₛ_eq

              theorem infₛ_sup_le_infᵢ_sup {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α} :
              infₛ s a b, h, b a

              This is a weaker version of infₛ_sup_eq

              theorem supᵢ_inf_le_supₛ_inf {α : Type u_1} [inst : CompleteLattice α] {a : α} {s : Set α} :
              (b, h, b a) supₛ s a

              This is a weaker version of supₛ_inf_eq

              theorem le_supᵢ_inf_supᵢ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ια) (g : ια) :
              (i, f i g i) (i, f i) i, g i
              theorem infᵢ_sup_infᵢ_le {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (f : ια) (g : ια) :
              ((i, f i) i, g i) i, f i g i
              theorem disjoint_supₛ_left {α : Type u_1} [inst : CompleteLattice α] {a : Set α} {b : α} (d : Disjoint (supₛ a) b) {i : α} (hi : i a) :
              theorem disjoint_supₛ_right {α : Type u_1} [inst : CompleteLattice α] {a : Set α} {b : α} (d : Disjoint b (supₛ a)) {i : α} (hi : i a) :
              def Function.Injective.completeLattice {α : Type u_1} {β : Type u_2} [inst : Sup α] [inst : Inf α] [inst : SupSet α] [inst : InfSet α] [inst : Top α] [inst : Bot α] [inst : 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_supₛ : ∀ (s : Set α), f (supₛ s) = a, h, f a) (map_infₛ : ∀ (s : Set α), f (infₛ s) = a, h, f a) (map_top : f = ) (map_bot : f = ) :

              Pullback a CompleteLattice along an injection.

              Equations
              • One or more equations did not get rendered due to their size.