Theory of complete lattices #
Main definitions #
Sup
andInf
are the supremum and the infimum of a set;supr (f : ι → α)
andinfi (f : ι → α)
are indexed supremum and infimum of a function, defined asSup
andInf
of the range of this function;class complete_lattice
: a bounded lattice such thatSup s
is always the least upper boundary ofs
andInf s
is always the greatest lower boundary ofs
;class complete_linear_order
: a linear ordered complete lattice.
Naming conventions #
In lemma names,
Sup
is calledSup
Inf
is calledInf
⨆ i, s i
is calledsupr
⨅ i, s i
is calledinfi
⨆ i j, s i j
is calledsupr₂
. This is asupr
inside asupr
.⨅ i j, s i j
is calledinfi₂
. This is aninfi
inside aninfi
.⨆ i ∈ s, t i
is calledbsupr
for "boundedsupr
". This is the special case ofsupr₂
wherej : i ∈ s
.⨅ i ∈ s, t i
is calledbinfi
for "boundedinfi
". This is the special case ofinfi₂
wherej : i ∈ s
.
Notation #
- Sup : set α → α
class for the Sup
operator
Instances of this typeclass
- complete_semilattice_Sup.to_has_Sup
- conditionally_complete_lattice.to_has_Sup
- order_dual.has_Sup
- pi.has_Sup
- prod.has_Sup
- set.has_Sup
- with_top.has_Sup
- with_bot.has_Sup
- nat.has_Sup
- order_hom.has_Sup
- real.has_Sup
- homogeneous_ideal.has_Sup
- tropical.has_Sup
- measure_theory.outer_measure.has_Sup
- ereal.has_Sup
- upper_set.has_Sup
- lower_set.has_Sup
- concept.has_Sup
- measure_theory.filtration.has_Sup
- ideal.filtration.has_Sup
Instances of other typeclasses for has_Sup
- has_Sup.has_sizeof_inst
- Inf : set α → α
class for the Inf
operator
Instances of this typeclass
- complete_semilattice_Inf.to_has_Inf
- conditionally_complete_lattice.to_has_Inf
- order_dual.has_Inf
- pi.has_Inf
- prod.has_Inf
- set.has_Inf
- setoid.has_Inf
- subsemigroup.has_Inf
- add_subsemigroup.has_Inf
- submonoid.has_Inf
- add_submonoid.has_Inf
- with_top.has_Inf
- with_bot.has_Inf
- nat.has_Inf
- subgroup.has_Inf
- add_subgroup.has_Inf
- subsemiring.has_Inf
- subring.has_Inf
- submodule.has_Inf
- order_hom.has_Inf
- con.has_Inf
- add_con.has_Inf
- subfield.has_Inf
- group_topology.has_Inf
- add_group_topology.has_Inf
- real.has_Inf
- uniform_space.has_Inf
- category_theory.grothendieck_topology.has_Inf
- homogeneous_ideal.has_Inf
- lie_subalgebra.has_Inf
- lie_submodule.has_Inf
- tropical.has_Inf
- measure_theory.measure.has_Inf
- ereal.has_Inf
- convex_cone.has_Inf
- upper_set.has_Inf
- lower_set.has_Inf
- projectivization.subspace.has_Inf
- first_order.language.substructure.has_Inf
- concept.has_Inf
- order.ideal.has_Inf
- measure_theory.filtration.has_Inf
- ideal.filtration.has_Inf
Instances of other typeclasses for has_Inf
- has_Inf.has_sizeof_inst
Indexed supremum
Equations
- supr s = has_Sup.Sup (set.range s)
Equations
- order_dual.has_Sup α = {Sup := has_Inf.Inf _inst_1}
Equations
- order_dual.has_Inf α = {Inf := has_Sup.Sup _inst_1}
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- Sup : set α → α
- le_Sup : ∀ (s : set α) (a : α), a ∈ s → a ≤ complete_semilattice_Sup.Sup s
- Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → complete_semilattice_Sup.Sup s ≤ a
Note that we rarely use complete_semilattice_Sup
(in fact, any such object is always a complete_lattice
, so it's usually best to start there).
Nevertheless it is sometimes a useful intermediate step in constructions.
Instances of this typeclass
Instances of other typeclasses for complete_semilattice_Sup
- complete_semilattice_Sup.has_sizeof_inst
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- Inf : set α → α
- Inf_le : ∀ (s : set α) (a : α), a ∈ s → complete_semilattice_Inf.Inf s ≤ a
- le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ complete_semilattice_Inf.Inf s
Note that we rarely use complete_semilattice_Inf
(in fact, any such object is always a complete_lattice
, so it's usually best to start there).
Nevertheless it is sometimes a useful intermediate step in constructions.
Instances of this typeclass
- complete_lattice.to_complete_semilattice_Inf
- fixed_points.function.fixed_points.complete_semilattice_Inf
- category_theory.subobject.complete_semilattice_Inf
- group_topology.complete_semilattice_Inf
- add_group_topology.complete_semilattice_Inf
- ring_topology.complete_semilattice_Inf
- measure_theory.measure.complete_semilattice_Inf
Instances of other typeclasses for complete_semilattice_Inf
- complete_semilattice_Inf.has_sizeof_inst
- sup : α → α → α
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
- le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
- sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c
- Sup : set α → α
- le_Sup : ∀ (s : set α) (a : α), a ∈ s → a ≤ complete_lattice.Sup s
- Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → complete_lattice.Sup s ≤ a
- Inf : set α → α
- Inf_le : ∀ (s : set α) (a : α), a ∈ s → complete_lattice.Inf s ≤ a
- le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ complete_lattice.Inf s
- top : α
- bot : α
- le_top : ∀ (x : α), x ≤ ⊤
- bot_le : ∀ (x : α), ⊥ ≤ x
A complete lattice is a bounded lattice which has suprema and infima for every subset.
Instances of this typeclass
- complete_linear_order.to_complete_lattice
- order.frame.to_complete_lattice
- order.coframe.to_complete_lattice
- order_dual.complete_lattice
- Prop.complete_lattice
- pi.complete_lattice
- prod.complete_lattice
- setoid.complete_lattice
- subsemigroup.complete_lattice
- add_subsemigroup.complete_lattice
- submonoid.complete_lattice
- add_submonoid.complete_lattice
- with_top.with_bot.complete_lattice
- subgroup.complete_lattice
- add_subgroup.complete_lattice
- subsemiring.complete_lattice
- subring.complete_lattice
- submodule.complete_lattice
- order_hom.complete_lattice
- con.complete_lattice
- add_con.complete_lattice
- fixed_points.function.fixed_points.complete_lattice
- algebra.subalgebra.complete_lattice
- subfield.complete_lattice
- category_theory.subobject.complete_lattice
- filter.complete_lattice
- rel.complete_lattice
- topological_space.complete_lattice
- topological_space.opens.complete_lattice
- topological_space.closeds.complete_lattice
- group_topology.complete_lattice
- add_group_topology.complete_lattice
- ring_topology.complete_lattice
- intermediate_field.complete_lattice
- uniform_space.complete_lattice
- affine_subspace.complete_lattice
- category_theory.presieve.complete_lattice
- category_theory.sieve.complete_lattice
- category_theory.grothendieck_topology.complete_lattice
- category_theory.morphism_property.complete_lattice
- homogeneous_ideal.complete_lattice
- lie_subalgebra.complete_lattice
- lie_submodule.complete_lattice
- measurable_space.complete_lattice
- measure_theory.outer_measure.complete_lattice
- measure_theory.measure.complete_lattice
- convex_cone.complete_lattice
- setoid.partition.complete_lattice
- projectivization.subspace.complete_lattice
- first_order.language.substructure.complete_lattice
- CompleteLattice.complete_lattice
- concept.complete_lattice
- order.ideal.complete_lattice
- measure_theory.filtration.complete_lattice
- ideal.filtration.complete_lattice
Instances of other typeclasses for complete_lattice
- complete_lattice.has_sizeof_inst
Equations
- complete_lattice.to_bounded_order = {top := complete_lattice.top h, le_top := _, bot := complete_lattice.bot h, bot_le := _}
Create a complete_lattice
from a partial_order
and Inf
function
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 complete_lattice
instance as
instance : complete_lattice my_T :=
{ inf := better_inf,
le_inf := ...,
inf_le_right := ...,
inf_le_left := ...
-- don't care to fix sup, Sup, bot, top
..complete_lattice_of_Inf my_T _ }
Equations
- complete_lattice_of_Inf α is_glb_Inf = {sup := λ (a b : α), has_Inf.Inf {x : α | a ≤ x ∧ b ≤ x}, le := partial_order.le H1, lt := partial_order.lt H1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (a b : α), has_Inf.Inf {a, b}, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := λ (s : set α), has_Inf.Inf (upper_bounds s), le_Sup := _, Sup_le := _, Inf := has_Inf.Inf H2, Inf_le := _, le_Inf := _, top := has_Inf.Inf ∅, bot := has_Inf.Inf set.univ, le_top := _, bot_le := _}
Any complete_semilattice_Inf
is in fact a complete_lattice
.
Note that this construction has bad definitional properties:
see the doc-string on complete_lattice_of_Inf
.
Equations
Create a complete_lattice
from a partial_order
and Sup
function
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 complete_lattice
instance as
instance : complete_lattice my_T :=
{ inf := better_inf,
le_inf := ...,
inf_le_right := ...,
inf_le_left := ...
-- don't care to fix sup, Inf, bot, top
..complete_lattice_of_Sup my_T _ }
Equations
- complete_lattice_of_Sup α is_lub_Sup = {sup := λ (a b : α), has_Sup.Sup {a, b}, le := partial_order.le H1, lt := partial_order.lt H1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (a b : α), has_Sup.Sup {x : α | x ≤ a ∧ x ≤ b}, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup H2, le_Sup := _, Sup_le := _, Inf := λ (s : set α), has_Sup.Sup (lower_bounds s), Inf_le := _, le_Inf := _, top := has_Sup.Sup set.univ, bot := has_Sup.Sup ∅, le_top := _, bot_le := _}
Any complete_semilattice_Sup
is in fact a complete_lattice
.
Note that this construction has bad definitional properties:
see the doc-string on complete_lattice_of_Sup
.
Equations
- sup : α → α → α
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
- lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
- le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
- le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
- le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
- sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c
- Sup : set α → α
- le_Sup : ∀ (s : set α) (a : α), a ∈ s → a ≤ complete_linear_order.Sup s
- Sup_le : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → b ≤ a) → complete_linear_order.Sup s ≤ a
- Inf : set α → α
- Inf_le : ∀ (s : set α) (a : α), a ∈ s → complete_linear_order.Inf s ≤ a
- le_Inf : ∀ (s : set α) (a : α), (∀ (b : α), b ∈ s → a ≤ b) → a ≤ complete_linear_order.Inf s
- top : α
- bot : α
- le_top : ∀ (x : α), x ≤ ⊤
- bot_le : ∀ (x : α), ⊥ ≤ x
- le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
- decidable_le : decidable_rel has_le.le
- decidable_eq : decidable_eq α
- decidable_lt : decidable_rel has_lt.lt
- max_def : complete_linear_order.sup = max_default . "reflexivity"
- min_def : complete_linear_order.inf = min_default . "reflexivity"
A complete linear order is a linear order whose lattice structure is complete.
Instances of this typeclass
- order_dual.complete_linear_order
- Prop.complete_linear_order
- with_top.complete_linear_order
- with_top.with_bot.complete_linear_order
- enat.complete_linear_order
- part_enat.complete_linear_order
- ennreal.complete_linear_order
- fin.complete_linear_order
- bool.complete_linear_order
- ereal.complete_linear_order
Instances of other typeclasses for complete_linear_order
- complete_linear_order.has_sizeof_inst
Equations
- order_dual.complete_lattice α = {sup := lattice.sup (order_dual.lattice α), le := lattice.le (order_dual.lattice α), lt := lattice.lt (order_dual.lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf (order_dual.lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup (order_dual.has_Sup α), le_Sup := _, Sup_le := _, Inf := has_Inf.Inf (order_dual.has_Inf α), Inf_le := _, le_Inf := _, top := bounded_order.top (order_dual.bounded_order α), bot := bounded_order.bot (order_dual.bounded_order α), le_top := _, bot_le := _}
Equations
- order_dual.complete_linear_order α = {sup := complete_lattice.sup (order_dual.complete_lattice α), le := complete_lattice.le (order_dual.complete_lattice α), lt := complete_lattice.lt (order_dual.complete_lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (order_dual.complete_lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (order_dual.complete_lattice α), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (order_dual.complete_lattice α), Inf_le := _, le_Inf := _, top := complete_lattice.top (order_dual.complete_lattice α), bot := complete_lattice.bot (order_dual.complete_lattice α), le_top := _, bot_le := _, le_total := _, decidable_le := linear_order.decidable_le (order_dual.linear_order α), decidable_eq := linear_order.decidable_eq (order_dual.linear_order α), decidable_lt := linear_order.decidable_lt (order_dual.linear_order α), max_def := _, min_def := _}
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.
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.
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 csupr_eq_of_forall_le_of_forall_lt_exists_gt
for a version in conditionally complete
lattices.
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 cinfi_eq_of_forall_ge_of_forall_gt_exists_lt
for a version in conditionally complete
lattices.
A version of supr_option
useful for rewriting right-to-left.
A version of infi_option
useful for rewriting right-to-left.
When taking the supremum of f : ι → α
, the elements of ι
on which f
gives ⊥
can be
dropped, without changing the result.
When taking the infimum of f : ι → α
, the elements of ι
on which f
gives ⊤
can be
dropped, without changing the result.
Instances #
Equations
- Prop.complete_lattice = {sup := distrib_lattice.sup Prop.distrib_lattice, le := distrib_lattice.le Prop.distrib_lattice, lt := distrib_lattice.lt Prop.distrib_lattice, le_refl := Prop.complete_lattice._proof_1, le_trans := Prop.complete_lattice._proof_2, lt_iff_le_not_le := Prop.complete_lattice._proof_3, le_antisymm := Prop.complete_lattice._proof_4, le_sup_left := Prop.complete_lattice._proof_5, le_sup_right := Prop.complete_lattice._proof_6, sup_le := Prop.complete_lattice._proof_7, inf := distrib_lattice.inf Prop.distrib_lattice, inf_le_left := Prop.complete_lattice._proof_8, inf_le_right := Prop.complete_lattice._proof_9, le_inf := Prop.complete_lattice._proof_10, Sup := λ (s : set Prop), ∃ (a : Prop) (H : a ∈ s), a, le_Sup := Prop.complete_lattice._proof_11, Sup_le := Prop.complete_lattice._proof_12, Inf := λ (s : set Prop), ∀ (a : Prop), a ∈ s → a, Inf_le := Prop.complete_lattice._proof_13, le_Inf := Prop.complete_lattice._proof_14, top := bounded_order.top Prop.bounded_order, bot := bounded_order.bot Prop.bounded_order, le_top := Prop.complete_lattice._proof_15, bot_le := Prop.complete_lattice._proof_16}
Equations
- Prop.complete_linear_order = {sup := complete_lattice.sup Prop.complete_lattice, le := complete_lattice.le Prop.complete_lattice, lt := complete_lattice.lt Prop.complete_lattice, le_refl := Prop.complete_linear_order._proof_1, le_trans := Prop.complete_linear_order._proof_2, lt_iff_le_not_le := Prop.complete_linear_order._proof_3, le_antisymm := Prop.complete_linear_order._proof_4, le_sup_left := Prop.complete_linear_order._proof_5, le_sup_right := Prop.complete_linear_order._proof_6, sup_le := Prop.complete_linear_order._proof_7, inf := complete_lattice.inf Prop.complete_lattice, inf_le_left := Prop.complete_linear_order._proof_8, inf_le_right := Prop.complete_linear_order._proof_9, le_inf := Prop.complete_linear_order._proof_10, Sup := complete_lattice.Sup Prop.complete_lattice, le_Sup := Prop.complete_linear_order._proof_11, Sup_le := Prop.complete_linear_order._proof_12, Inf := complete_lattice.Inf Prop.complete_lattice, Inf_le := Prop.complete_linear_order._proof_13, le_Inf := Prop.complete_linear_order._proof_14, top := complete_lattice.top Prop.complete_lattice, bot := complete_lattice.bot Prop.complete_lattice, le_top := Prop.complete_linear_order._proof_15, bot_le := Prop.complete_linear_order._proof_16, le_total := Prop.complete_linear_order._proof_17, decidable_le := linear_order.decidable_le Prop.linear_order, decidable_eq := linear_order.decidable_eq Prop.linear_order, decidable_lt := linear_order.decidable_lt Prop.linear_order, max_def := Prop.complete_linear_order._proof_18, min_def := Prop.complete_linear_order._proof_19}
Equations
- pi.complete_lattice = {sup := lattice.sup pi.lattice, le := lattice.le pi.lattice, lt := lattice.lt pi.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf pi.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup pi.has_Sup, le_Sup := _, Sup_le := _, Inf := has_Inf.Inf pi.has_Inf, Inf_le := _, le_Inf := _, top := bounded_order.top pi.bounded_order, bot := bounded_order.bot pi.bounded_order, le_top := _, bot_le := _}
Equations
- prod.has_Sup α β = {Sup := λ (s : set (α × β)), (has_Sup.Sup (prod.fst '' s), has_Sup.Sup (prod.snd '' s))}
Equations
- prod.has_Inf α β = {Inf := λ (s : set (α × β)), (has_Inf.Inf (prod.fst '' s), has_Inf.Inf (prod.snd '' s))}
Equations
- prod.complete_lattice α β = {sup := lattice.sup (prod.lattice α β), le := lattice.le (prod.lattice α β), lt := lattice.lt (prod.lattice α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf (prod.lattice α β), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup (prod.has_Sup α β), le_Sup := _, Sup_le := _, Inf := has_Inf.Inf (prod.has_Inf α β), Inf_le := _, le_Inf := _, top := bounded_order.top (prod.bounded_order α β), bot := bounded_order.bot (prod.bounded_order α β), le_top := _, bot_le := _}
This is a weaker version of sup_Inf_eq
This is a weaker version of inf_Sup_eq
This is a weaker version of Inf_sup_eq
This is a weaker version of Sup_inf_eq
Pullback a complete_lattice
along an injection.
Equations
- function.injective.complete_lattice f hf map_sup map_inf map_Sup map_Inf map_top map_bot = {sup := lattice.sup (function.injective.lattice f hf map_sup map_inf), le := lattice.le (function.injective.lattice f hf map_sup map_inf), lt := lattice.lt (function.injective.lattice f hf map_sup map_inf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf (function.injective.lattice f hf map_sup map_inf), inf_le_left := _, inf_le_right := _, le_inf := _, Sup := has_Sup.Sup _inst_3, le_Sup := _, Sup_le := _, Inf := has_Inf.Inf _inst_4, Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}