English
WithBot(Box ι) forms a lattice with infimum defined coordinatewise; the order corresponds to subset inclusion of the sets.
Русский
Система WithBot(Box ι) образует решётку: наименьшее по координатам инфимума задаётся по координатам; порядок соответствует подмножеству множеств.
LaTeX
$$$\text{WithBot(Box ι)}\;\text{is a lattice with inf = coordinatewise min and } I \le J \text{ iff } I.toSet \subseteq J.toSet$$$
Lean4
instance : Lattice (WithBot (Box ι)) :=
{ inf := min
inf_le_left := fun I J ↦ by
rw [← withBotCoe_subset_iff, coe_inf]
exact inter_subset_left
inf_le_right := fun I J ↦ by
rw [← withBotCoe_subset_iff, coe_inf]
exact inter_subset_right
le_inf := fun I J₁ J₂ h₁ h₂ ↦ by
simp only [← withBotCoe_subset_iff, coe_inf] at *
exact subset_inter h₁ h₂ }
