English
The real numbers form a distributive lattice with sup and inf; the distributive law holds: a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c).
Русский
Действительные образуют дистрибутивную решётку; выполняется распределительная закон: a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c).
LaTeX
$$$\forall a,b,c\in\mathbb{R},\ a \wedge (b \vee c) = (a \wedge b) \vee (a \wedge c)$$$
Lean4
instance : DistribLattice ℝ :=
{ Real.partialOrder with
sup := (· ⊔ ·)
le := (· ≤ ·)
le_sup_left := by
intro a b
induction a using Real.ind_mk
induction b using Real.ind_mk
dsimp only; rw [← mk_sup, mk_le]
exact CauSeq.le_sup_left
le_sup_right := by
intro a b
induction a using Real.ind_mk
induction b using Real.ind_mk
dsimp only; rw [← mk_sup, mk_le]
exact CauSeq.le_sup_right
sup_le := by
intro a b c
induction a using Real.ind_mk
induction b using Real.ind_mk
induction c using Real.ind_mk
simp_rw [← mk_sup, mk_le]
exact CauSeq.sup_le
inf := (· ⊓ ·)
inf_le_left := by
intro a b
induction a using Real.ind_mk
induction b using Real.ind_mk
dsimp only; rw [← mk_inf, mk_le]
exact CauSeq.inf_le_left
inf_le_right := by
intro a b
induction a using Real.ind_mk
induction b using Real.ind_mk
dsimp only; rw [← mk_inf, mk_le]
exact CauSeq.inf_le_right
le_inf := by
intro a b c
induction a using Real.ind_mk
induction b using Real.ind_mk
induction c using Real.ind_mk
simp_rw [← mk_inf, mk_le]
exact CauSeq.le_inf
le_sup_inf := by
intro a b c
induction a using Real.ind_mk
induction b using Real.ind_mk
induction c using Real.ind_mk
apply Eq.le
simp only [← mk_sup, ← mk_inf]
exact congr_arg mk (CauSeq.sup_inf_distrib_left ..).symm }
-- Extra instances to short-circuit type class resolution
