⊤ and ⊥, bounded lattices and variants #
This file defines top and bottom elements (greatest and least elements) of a type, the bounded
variants of different kinds of lattices, sets up the typeclass hierarchy between them and provides
instances for Prop
and fun
.
Main declarations #
has_<top/bot> α
: Typeclasses to declare the⊤
/⊥
notation.order_<top/bot> α
: Order with a top/bottom element.bounded_order α
: Order with a top and bottom element.with_<top/bot> α
: Equipsoption α
with the order onα
plusnone
as the top/bottom element.is_compl x y
: In a bounded lattice, predicate for "x
is a complement ofy
". Note that in a non distributive lattice, an element can have several complements.complemented_lattice α
: Typeclass stating that any element of a lattice has a complement.
Common lattices #
- Distributive lattices with a bottom element. Notated by
[distrib_lattice α] [order_bot α]
It captures the properties ofdisjoint
that are common togeneralized_boolean_algebra
anddistrib_lattice
whenorder_bot
. - Bounded and distributive lattice. Notated by
[distrib_lattice α] [bounded_order α]
. Typical examples includeProp
andset α
.
Top, bottom element #
- top : α
Typeclass for the ⊤
(\top
) notation
Instances of this typeclass
- order_top.to_has_top
- generalized_heyting_algebra.to_has_top
- coheyting_algebra.to_has_top
- boolean_algebra.to_has_top
- linear_ordered_add_comm_monoid_with_top.to_has_top
- complete_lattice.to_has_top
- order_dual.has_top
- pi.has_top
- with_top.has_top
- prod.has_top
- subsemigroup.has_top
- add_subsemigroup.has_top
- submonoid.has_top
- add_submonoid.has_top
- subgroup.has_top
- add_subgroup.has_top
- subsemiring.has_top
- subring.has_top
- associates.has_top
- submodule.has_top
- order_hom.has_top
- enat.has_top
- part_enat.has_top
- subfield.has_top
- sup_hom.has_top
- inf_hom.has_top
- category_theory.mono_over.has_top
- filter.has_top
- Inf_hom.has_top
- topological_space.clopens.has_top
- topological_space.compacts.has_top
- topological_space.nonempty_compacts.has_top
- topological_space.positive_compacts.has_top
- topological_space.compact_opens.has_top
- group_topology.has_top
- add_group_topology.has_top
- uniform_space.has_top
- homogeneous_ideal.has_top
- lie_subalgebra.has_top
- lie_submodule.has_top
- star_subalgebra.has_top
- tropical.has_top
- measurable_set.subtype.has_top
- ereal.has_top
- filter.germ.has_top
- convex_cone.has_top
- enorm.has_top
- category_theory.grothendieck_topology.subpresheaf.has_top
- quiver.wide_subquiver.has_top
- upper_set.has_top
- lower_set.has_top
- open_subgroup.has_top
- open_add_subgroup.has_top
- first_order.language.bounded_formula.has_top
- first_order.language.substructure.has_top
- first_order.language.elementary_substructure.has_top
- first_order.language.definable_set.has_top
- heyting.regular.has_top
- measure_theory.filtration.has_top
- valuation_subring.has_top
- ideal.filtration.has_top
- clopen_upper_set.has_top
Instances of other typeclasses for has_top
- has_top.has_sizeof_inst
- bot : α
Typeclass for the ⊥
(\bot
) notation
Instances of this typeclass
- order_bot.to_has_bot
- generalized_coheyting_algebra.to_has_bot
- heyting_algebra.to_has_bot
- generalized_boolean_algebra.to_has_bot
- boolean_algebra.to_has_bot
- canonically_ordered_add_monoid.to_has_bot
- canonically_ordered_monoid.to_has_bot
- complete_lattice.to_has_bot
- conditionally_complete_linear_order_bot.to_has_bot
- order_dual.has_bot
- pi.has_bot
- with_bot.has_bot
- prod.has_bot
- subsemigroup.has_bot
- add_subsemigroup.has_bot
- submonoid.has_bot
- add_submonoid.has_bot
- subgroup.has_bot
- add_subgroup.has_bot
- subsemiring.has_bot
- subring.has_bot
- sub_mul_action.has_bot
- associates.has_bot
- submodule.has_bot
- order_hom.has_bot
- enat.has_bot
- part_enat.has_bot
- linear_pmap.has_bot
- pequiv.has_bot
- sup_hom.has_bot
- inf_hom.has_bot
- category_theory.mono_over.has_bot
- Sup_hom.has_bot
- topological_space.clopens.has_bot
- topological_space.compacts.has_bot
- topological_space.compact_opens.has_bot
- group_topology.has_bot
- add_group_topology.has_bot
- uniform_space.has_bot
- homogeneous_ideal.has_bot
- lie_subalgebra.has_bot
- lie_submodule.has_bot
- measure_theory.outer_measure.has_bot
- measurable_set.subtype.has_bot
- ereal.has_bot
- filter.germ.has_bot
- convex_cone.has_bot
- geometry.simplicial_complex.has_bot
- quiver.wide_subquiver.has_bot
- upper_set.has_bot
- lower_set.has_bot
- finpartition.has_bot
- first_order.language.bounded_formula.has_bot
- first_order.language.definable_set.has_bot
- heyting.regular.has_bot
- measure_theory.filtration.has_bot
- ideal.filtration.has_bot
- clopen_upper_set.has_bot
Instances of other typeclasses for has_bot
- has_bot.has_sizeof_inst
An order is an order_top
if it has a greatest element.
We state this using a data mixin, holding the value of ⊤
and the greatest element constraint.
Instances of this typeclass
- bounded_order.to_order_top
- generalized_heyting_algebra.to_order_top
- linear_ordered_add_comm_monoid_with_top.to_order_top
- order_dual.order_top
- pi.order_top
- with_bot.order_top
- with_top.order_top
- prod.order_top
- multiplicative.order_top
- additive.order_top
- set.order_top
- pi.lex.order_top
- finset.order_top
- set.Iic.order_top
- set.Ici.order_top
- associates.order_top
- submodule.order_top
- flag.order_top
- order_hom.order_top
- enat.order_top
- part_enat.order_top
- sum.lex.order_top
- ordinal.order_top_out_succ
- top_hom.order_top
- sup_hom.order_top
- inf_hom.order_top
- inf_top_hom.order_top
- SemilatticeInf.is_order_top
- category_theory.subobject.order_top
- Inf_hom.order_top
- topological_space.nonempty_compacts.order_top
- topological_space.positive_compacts.order_top
- category_theory.grothendieck_topology.cover.order_top
- category_theory.pretopology.order_top
- topological_space.open_nhds.order_top
- tropical.order_top
- box_integral.prepartition.order_top
- measure_theory.simple_func.order_top
- filter.germ.order_top
- enorm.order_top
- colex.finset.colex.order_top
- finpartition.order_top
- semiquot.order_top
- sigma.lex.order_top
- open_subgroup.order_top
- open_add_subgroup.order_top
- structure_groupoid.order_top
- order.ideal.order_top
- order.pfilter.order_top
- valuation_subring.order_top
- discrete_quotient.order_top
Instances of other typeclasses for order_top
- order_top.has_sizeof_inst
An order is (noncomputably) either an order_top
or a no_order_top
. Use as
casesI bot_order_or_no_bot_order α
.
Alias of ne_top_of_lt
.
Alias of the forward direction of is_max_iff_eq_top
.
Alias of the forward direction of is_top_iff_eq_top
.
An order is an order_bot
if it has a least element.
We state this using a data mixin, holding the value of ⊥
and the least element constraint.
Instances of this typeclass
- bounded_order.to_order_bot
- generalized_coheyting_algebra.to_order_bot
- generalized_boolean_algebra.to_order_bot
- canonically_ordered_add_monoid.to_order_bot
- canonically_ordered_monoid.to_order_bot
- conditionally_complete_linear_order_bot.to_order_bot
- order_dual.order_bot
- pi.order_bot
- with_bot.order_bot
- with_top.order_bot
- prod.order_bot
- with_zero.order_bot
- multiplicative.order_bot
- additive.order_bot
- nat.order_bot
- nat.subtype.order_bot
- pnat.order_bot
- pi.lex.order_bot
- multiset.order_bot
- finset.order_bot
- set.Iic.order_bot
- set.Ici.order_bot
- associates.order_bot
- submodule.order_bot
- flag.order_bot
- part.order_bot
- order_hom.order_bot
- enat.order_bot
- part_enat.order_bot
- linear_pmap.order_bot
- finsupp.order_bot
- sum.lex.order_bot
- ordinal.order_bot
- set_semiring.order_bot
- pequiv.order_bot
- bot_hom.order_bot
- sup_hom.order_bot
- inf_hom.order_bot
- sup_bot_hom.order_bot
- SemilatticeSup.is_order_bot
- category_theory.subobject.order_bot
- Sup_hom.order_bot
- topological_space.compacts.order_bot
- topological_space.compact_opens.order_bot
- intermediate_field.lifts.order_bot
- nonneg.order_bot
- nnreal.order_bot
- category_theory.pretopology.order_bot
- fractional_ideal.order_bot
- box_integral.prepartition.order_bot
- measure_theory.outer_measure.outer_measure.order_bot
- measure_theory.simple_func.order_bot
- filter.germ.order_bot
- seminorm.order_bot
- geometry.simplicial_complex.order_bot
- colex.finset.colex.order_bot
- finpartition.order_bot
- young_diagram.order_bot
- dfinsupp.order_bot
- prime_multiset.order_bot
- sigma.lex.order_bot
- structure_groupoid.order_bot
- order.ideal.order_bot
- order.pfilter.order_bot
- discrete_quotient.order_bot
Instances of other typeclasses for order_bot
- order_bot.has_sizeof_inst
An order is (noncomputably) either an order_bot
or a no_order_bot
. Use as
casesI bot_order_or_no_bot_order α
.
Equations
- order_dual.has_top α = {top := ⊥}
Equations
- order_dual.has_bot α = {bot := ⊤}
Alias of ne_bot_of_gt
.
Alias of the forward direction of is_min_iff_eq_bot
.
Alias of the forward direction of is_bot_iff_eq_bot
.
Bounded order #
A bounded order describes an order (≤)
with a top and bottom element,
denoted ⊤
and ⊥
respectively.
Instances of this typeclass
- heyting_algebra.to_bounded_order
- coheyting_algebra.to_bounded_order
- boolean_algebra.to_bounded_order
- complete_lattice.to_bounded_order
- nonempty_fin_lin_ord.to_bounded_order
- order_dual.bounded_order
- Prop.bounded_order
- pi.bounded_order
- with_bot.bounded_order
- with_top.bounded_order
- prod.bounded_order
- bool.bounded_order
- multiplicative.bounded_order
- additive.bounded_order
- fin.bounded_order
- pi.lex.bounded_order
- set.Iic.bounded_order
- set.Ici.bounded_order
- associates.bounded_order
- flag.bounded_order
- part_enat.bounded_order
- sum.lex.bounded_order
- sup_hom.bounded_order
- inf_hom.bounded_order
- BoundedOrder.is_bounded_order
- BoundedLattice.is_bounded_order
- BoundedDistribLattice.is_bounded_order
- category_theory.subobject.bounded_order
- topological_space.compacts.bounded_order
- topological_space.compact_opens.bounded_order
- group_topology.bounded_order
- add_group_topology.bounded_order
- sign_type.bounded_order
- box_integral.integration_params.bounded_order
- measurable_set.subtype.bounded_order
- measure_theory.simple_func.bounded_order
- filter.germ.bounded_order
- is_Lprojection.subtype.bounded_order
- colex.finset.colex.bounded_order
- simple_graph.subgraph.bounded_order
- sigma.lex.bounded_order
- first_order.language.definable_set.bounded_order
- concept.bounded_order
- heyting.regular.bounded_order
- clopen_upper_set.bounded_order
Instances of other typeclasses for bounded_order
- bounded_order.has_sizeof_inst
Equations
- order_dual.bounded_order α = {top := order_top.top (order_dual.order_top α), le_top := _, bot := order_bot.bot (order_dual.order_bot α), bot_le := _}
Propositions form a distributive lattice.
Equations
- Prop.distrib_lattice = {sup := or, le := partial_order.le Prop.partial_order, lt := partial_order.lt Prop.partial_order, le_refl := Prop.distrib_lattice._proof_1, le_trans := Prop.distrib_lattice._proof_2, lt_iff_le_not_le := Prop.distrib_lattice._proof_3, le_antisymm := Prop.distrib_lattice._proof_4, le_sup_left := or.inl, le_sup_right := or.inr, sup_le := Prop.distrib_lattice._proof_5, inf := and, inf_le_left := and.left, inf_le_right := and.right, le_inf := Prop.distrib_lattice._proof_6, le_sup_inf := Prop.distrib_lattice._proof_7}
Propositions form a bounded order.
Equations
- Prop.bounded_order = {top := true, le_top := Prop.bounded_order._proof_1, bot := false, bot_le := false.elim}
Equations
In this section we prove some properties about monotone and antitone operations on Prop
#
Function lattices #
Equations
- pi.has_bot = {bot := λ (i : ι), ⊥}
Equations
- pi.has_top = {top := λ (i : ι), ⊤}
Equations
- pi.bounded_order = {top := order_top.top pi.order_top, le_top := _, bot := order_bot.bot pi.order_bot, bot_le := _}
Pullback a bounded_order
.
Equations
- bounded_order.lift f map_le map_top map_bot = {top := order_top.top (order_top.lift f map_le map_top), le_top := _, bot := order_bot.bot (order_bot.lift f map_le map_bot), bot_le := _}
Attach ⊥
to a type.
Instances for with_bot
- with_bot.has_le
- with_bot.has_lt
- with_bot.has_to_format
- with_bot.has_repr
- with_bot.has_coe_t
- with_bot.has_bot
- with_bot.has_reflect
- with_bot.inhabited
- with_bot.can_lift
- with_bot.order_bot
- with_bot.order_top
- with_bot.bounded_order
- with_bot.preorder
- with_bot.partial_order
- with_bot.semilattice_sup
- with_bot.semilattice_inf
- with_bot.lattice
- with_bot.is_total_le
- with_bot.linear_order
- with_bot.densely_ordered
- with_bot.no_top_order
- with_bot.no_max_order
- with_bot.trichotomous.lt
- with_bot.is_well_order.lt
- with_bot.trichotomous.gt
- with_bot.is_well_order.gt
- with_bot.has_one
- with_bot.has_zero
- with_bot.has_add
- with_bot.add_semigroup
- with_bot.add_comm_semigroup
- with_bot.add_zero_class
- with_bot.add_monoid
- with_bot.add_comm_monoid
- with_bot.add_monoid_with_one
- with_bot.add_comm_monoid_with_one
- with_bot.zero_le_one_class
- with_bot.covariant_class_add_le
- with_bot.covariant_class_swap_add_le
- with_bot.contravariant_class_add_lt
- with_bot.contravariant_class_swap_add_lt
- with_bot.ordered_add_comm_monoid
- with_bot.linear_ordered_add_comm_monoid
- with_bot.nontrivial
- with_bot.mul_zero_class
- with_bot.mul_zero_one_class
- with_bot.no_zero_divisors
- with_bot.semigroup_with_zero
- with_bot.monoid_with_zero
- with_bot.comm_monoid_with_zero
- with_bot.comm_semiring
- with_bot.zero_lt.pos_mul_mono
- with_bot.zero_lt.mul_pos_mono
- with_bot.has_Sup
- with_bot.has_Inf
- with_bot.conditionally_complete_lattice
- with_bot.locally_finite_order
- with_bot.succ_order
- with_bot.pred_order
- with_bot.pred_order_of_no_min_order
- box_integral.box.with_bot_coe
- box_integral.box.with_bot.has_inf
- box_integral.box.with_bot.lattice
Equations
- with_bot.has_repr = {repr := λ (o : with_bot α), with_bot.has_repr._match_1 o}
- with_bot.has_repr._match_1 (option.some a) = "↑" ++ repr a
- with_bot.has_repr._match_1 option.none = "⊥"
Equations
- with_bot.has_coe_t = {coe := option.some α}
Equations
- with_bot.has_bot = {bot := option.none α}
Equations
- with_bot.inhabited = {default := ⊥}
Recursor for with_bot
using the preferred forms ⊥
and ↑a
.
Equations
- with_bot.rec_bot_coe h₁ h₂ = option.rec h₁ h₂
Specialization of option.get_or_else
to values in with_bot α
that respects API boundaries.
Equations
- with_bot.unbot' d x = with_bot.rec_bot_coe d id x
Lift a map f : α → β
to with_bot α → with_bot β
. Implemented using option.map
.
Equations
- with_bot.map f = option.map f
Deconstruct a x : with_bot α
to the underlying value in α
, given a proof that x ≠ ⊥
.
Equations
- with_bot.unbot (option.some x) h = x
- ⊥.unbot h = absurd with_bot.unbot._main._proof_1 h
Equations
- with_bot.order_top = {top := option.some ⊤, le_top := _}
Equations
- with_bot.bounded_order = {top := order_top.top with_bot.order_top, le_top := _, bot := order_bot.bot with_bot.order_bot, bot_le := _}
Equations
- with_bot.preorder = {le := has_le.le with_bot.has_le, lt := has_lt.lt with_bot.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
Equations
- with_bot.partial_order = {le := preorder.le with_bot.preorder, lt := preorder.lt with_bot.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Equations
- with_bot.semilattice_sup = {sup := option.lift_or_get has_sup.sup, le := partial_order.le with_bot.partial_order, lt := partial_order.lt with_bot.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}
Equations
- with_bot.semilattice_inf = {inf := λ (o₁ o₂ : with_bot α), option.bind o₁ (λ (a : α), with_bot.map (λ (b : α), a ⊓ b) o₂), le := partial_order.le with_bot.partial_order, lt := partial_order.lt with_bot.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
Equations
- with_bot.lattice = {sup := semilattice_sup.sup with_bot.semilattice_sup, le := semilattice_sup.le with_bot.semilattice_sup, lt := semilattice_sup.lt with_bot.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf with_bot.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
Equations
- with_bot.decidable_le (option.some x) (option.some y) = dite (x ≤ y) (λ (h : x ≤ y), decidable.is_true _) (λ (h : ¬x ≤ y), decidable.is_false _)
- with_bot.decidable_le (option.some x) option.none = decidable.is_false _
- with_bot.decidable_le option.none x = decidable.is_true _
Equations
- with_bot.decidable_lt (option.some x) (option.some y) = dite (x < y) (λ (h : x < y), decidable.is_true _) (λ (h : ¬x < y), decidable.is_false _)
- with_bot.decidable_lt (option.some val) option.none = decidable.is_false _
- with_bot.decidable_lt option.none (option.some x) = decidable.is_true _
- with_bot.decidable_lt option.none option.none = decidable.is_false with_bot.decidable_lt._main._proof_1
Equations
Attach ⊤
to a type.
Instances for with_top
- with_top.has_le
- with_top.has_lt
- with_top.has_to_format
- with_top.has_repr
- with_top.has_coe_t
- with_top.has_top
- with_top.has_reflect
- with_top.inhabited
- with_top.can_lift
- with_top.order_top
- with_top.order_bot
- with_top.bounded_order
- with_top.preorder
- with_top.partial_order
- with_top.semilattice_inf
- with_top.semilattice_sup
- with_top.lattice
- with_top.is_total_le
- with_top.linear_order
- with_top.trichotomous.lt
- with_top.is_well_order.lt
- with_top.trichotomous.gt
- with_top.is_well_order.gt
- with_top.densely_ordered
- with_top.no_bot_order
- with_top.no_min_order
- with_top.has_one
- with_top.has_zero
- with_top.zero_le_one_class
- with_top.has_add
- with_top.covariant_class_add_le
- with_top.covariant_class_swap_add_le
- with_top.contravariant_class_add_lt
- with_top.contravariant_class_swap_add_lt
- with_top.add_semigroup
- with_top.add_comm_semigroup
- with_top.add_zero_class
- with_top.add_monoid
- with_top.add_comm_monoid
- with_top.add_monoid_with_one
- with_top.add_comm_monoid_with_one
- with_top.ordered_add_comm_monoid
- with_top.linear_ordered_add_comm_monoid_with_top
- with_top.has_exists_add_of_le
- with_top.canonically_ordered_add_monoid
- with_top.canonically_linear_ordered_add_monoid
- with_top.has_sub
- with_top.has_ordered_sub
- with_top.linear_ordered_add_comm_group_with_top
- with_top.nontrivial
- with_top.mul_zero_class
- with_top.mul_zero_one_class
- with_top.no_zero_divisors
- with_top.semigroup_with_zero
- with_top.monoid_with_zero
- with_top.comm_monoid_with_zero
- with_top.comm_semiring
- with_top.canonically_ordered_comm_semiring
- with_top.char_zero
- with_top.has_Sup
- with_top.has_Inf
- with_top.complete_linear_order
- with_top.conditionally_complete_lattice
- with_top.with_bot.complete_lattice
- with_top.with_bot.complete_linear_order
- with_top.locally_finite_order
- with_top.succ_order
- with_top.pred_order
- with_top.succ_order_of_no_max_order
- associates.factor_set.has_mem
Equations
- with_top.has_repr = {repr := λ (o : with_top α), with_top.has_repr._match_1 o}
- with_top.has_repr._match_1 (option.some a) = "↑" ++ repr a
- with_top.has_repr._match_1 option.none = "⊤"
Equations
- with_top.has_coe_t = {coe := option.some α}
Equations
- with_top.has_top = {top := option.none α}
Equations
- with_top.inhabited = {default := ⊤}
Recursor for with_top
using the preferred forms ⊤
and ↑a
.
Equations
- with_top.rec_top_coe h₁ h₂ = option.rec h₁ h₂
with_top.to_dual
is the equivalence sending ⊤
to ⊥
and any a : α
to to_dual a : αᵒᵈ
.
See with_top.to_dual_bot_equiv
for the related order-iso.
Equations
with_top.of_dual
is the equivalence sending ⊤
to ⊥
and any a : αᵒᵈ
to of_dual a : α
.
See with_top.to_dual_bot_equiv
for the related order-iso.
Equations
with_bot.to_dual
is the equivalence sending ⊥
to ⊤
and any a : α
to to_dual a : αᵒᵈ
.
See with_bot.to_dual_top_equiv
for the related order-iso.
Equations
with_bot.of_dual
is the equivalence sending ⊥
to ⊤
and any a : αᵒᵈ
to of_dual a : α
.
See with_bot.to_dual_top_equiv
for the related order-iso.
Equations
Specialization of option.get_or_else
to values in with_top α
that respects API boundaries.
Equations
- with_top.untop' d x = with_top.rec_top_coe d id x
Lift a map f : α → β
to with_top α → with_top β
. Implemented using option.map
.
Equations
- with_top.map f = option.map f
Deconstruct a x : with_top α
to the underlying value in α
, given a proof that x ≠ ⊤
.
Equations
Equations
- with_top.order_bot = {bot := option.some ⊥, bot_le := _}
Equations
- with_top.bounded_order = {top := order_top.top with_top.order_top, le_top := _, bot := order_bot.bot with_top.order_bot, bot_le := _}
Equations
- with_top.preorder = {le := has_le.le with_top.has_le, lt := has_lt.lt with_top.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}
Equations
- with_top.partial_order = {le := preorder.le with_top.preorder, lt := preorder.lt with_top.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
Equations
- with_top.semilattice_inf = {inf := option.lift_or_get has_inf.inf, le := partial_order.le with_top.partial_order, lt := partial_order.lt with_top.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
Equations
- with_top.semilattice_sup = {sup := λ (o₁ o₂ : with_top α), option.bind o₁ (λ (a : α), with_top.map (λ (b : α), a ⊔ b) o₂), le := partial_order.le with_top.partial_order, lt := partial_order.lt with_top.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}
Equations
- with_top.lattice = {sup := semilattice_sup.sup with_top.semilattice_sup, le := semilattice_sup.le with_top.semilattice_sup, lt := semilattice_sup.lt with_top.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf with_top.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
Equations
- with_top.decidable_le = λ (_x _x_1 : with_top α), decidable_of_decidable_of_iff (with_bot.decidable_le (⇑with_top.to_dual _x_1) (⇑with_top.to_dual _x)) with_top.to_dual_le_to_dual_iff
Equations
- with_top.decidable_lt = λ (_x _x_1 : with_top α), decidable_of_decidable_of_iff (with_bot.decidable_lt (⇑with_top.to_dual _x_1) (⇑with_top.to_dual _x)) with_top.to_dual_lt_to_dual_iff
Equations
Subtype, order dual, product lattices #
A subtype remains a bounded order if the property holds at ⊥
and ⊤
.
Equations
- subtype.bounded_order hbot htop = {top := order_top.top (subtype.order_top htop), le_top := _, bot := order_bot.bot (subtype.order_bot hbot), bot_le := _}
Equations
- prod.bounded_order α β = {top := order_top.top (prod.order_top α β), le_top := _, bot := order_bot.bot (prod.order_bot α β), bot_le := _}
Disjointness and complements #
Two elements of a lattice are disjoint if their inf is the bottom element. (This generalizes disjoint sets, viewed as members of the subset lattice.)
Instances for disjoint
Alias of the forward direction of disjoint_self
.
Two elements of a lattice are codisjoint if their sup is the top element.
Equations
- codisjoint a b = (⊤ ≤ a ⊔ b)
Alias of the forward direction of codisjoint_self
.
- disjoint : disjoint x y
- codisjoint : codisjoint x y
Two elements x
and y
are complements of each other if x ⊔ y = ⊤
and x ⊓ y = ⊥
.
- exists_is_compl : ∀ (a : α), ∃ (b : α), is_compl a b
A complemented bounded lattice is one where every element has a (not necessarily unique) complement.
Instances of this typeclass
- boolean_algebra.to_complemented_lattice
- complemented_lattice.order_dual.complemented_lattice
- is_modular_lattice.complemented_lattice_Iic
- is_modular_lattice.complemented_lattice_Ici
- module.submodule.complemented_lattice
- is_semisimple_module.is_semisimple_submodule
- monoid_algebra.submodule.complemented_lattice