English
a ⊓ b = a ⊓ c ↔ a ⊓ c ≤ b ∧ a ⊓ b ≤ c.
Русский
a ⊓ b = a ⊓ c эквивалентно a ⊓ c ≤ b и a ⊓ b ≤ c.
LaTeX
$$$ \forall a,b,c : \alpha,\ Iff (a \wedge b) (a \wedge c) \ (And (a \wedge c \le b) (a \wedge b \le c)) $$$
Lean4
/-- A type with a pair of commutative and associative binary operations which satisfy two absorption
laws relating the two operations has the structure of a lattice.
The partial order is defined so that `a ≤ b` unfolds to `a ⊔ b = b`; cf. `sup_eq_right`.
-/
def mk' {α : Type*} [Max α] [Min α] (sup_comm : ∀ a b : α, a ⊔ b = b ⊔ a)
(sup_assoc : ∀ a b c : α, a ⊔ b ⊔ c = a ⊔ (b ⊔ c)) (inf_comm : ∀ a b : α, a ⊓ b = b ⊓ a)
(inf_assoc : ∀ a b c : α, a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (sup_inf_self : ∀ a b : α, a ⊔ a ⊓ b = a)
(inf_sup_self : ∀ a b : α, a ⊓ (a ⊔ b) = a) : Lattice α :=
have sup_idem : ∀ b : α, b ⊔ b = b := fun b =>
calc
b ⊔ b = b ⊔ b ⊓ (b ⊔ b) := by rw [inf_sup_self]
_ = b := by rw [sup_inf_self]
have inf_idem : ∀ b : α, b ⊓ b = b := fun b =>
calc
b ⊓ b = b ⊓ (b ⊔ b ⊓ b) := by rw [sup_inf_self]
_ = b := by rw [inf_sup_self]
let semilatt_inf_inst := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
let semilatt_sup_inst := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
have partial_order_eq :
@SemilatticeSup.toPartialOrder _ semilatt_sup_inst = @SemilatticeInf.toPartialOrder _ semilatt_inf_inst :=
semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder _ _ _ _ _ _ sup_inf_self inf_sup_self
{ semilatt_sup_inst, semilatt_inf_inst with
inf_le_left := fun a b => by
rw [partial_order_eq]
apply inf_le_left,
inf_le_right := fun a b => by
rw [partial_order_eq]
apply inf_le_right,
le_inf := fun a b c => by
rw [partial_order_eq]
apply le_inf }
