English
Distributivity of join over meet on CauSeq: a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c).
Русский
Сумма верхних границ над нижними границами раскладывается слева: a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c).
LaTeX
$$$a,b,c \in \mathrm{CauSeq}(\alpha, \mathrm{abs}) \,\Rightarrow\; a \vee (b \wedge c) = (a \vee b) \wedge (a \vee c)$$$
Lean4
protected theorem le_inf {a b c : CauSeq α abs} (hb : a ≤ b) (hc : a ≤ c) : a ≤ b ⊓ c :=
by
obtain hb | hb := hb
· obtain hc | hc := hc
· exact Or.inl (CauSeq.lt_inf hb hc)
· replace hb := le_of_eq_of_le (Setoid.symm hc) hb.le
refine le_of_eq_of_le hc (Or.inr ?_)
exact Setoid.symm (CauSeq.inf_eq_right hb)
· replace hc := le_of_eq_of_le (Setoid.symm hb) hc
refine le_of_eq_of_le hb (Or.inr ?_)
exact Setoid.symm (CauSeq.inf_eq_left hc)
