English
The underlying set of the infimum of two intervals equals the intersection of their underlying sets.
Русский
Нижняя граница двух интервалов соответствует пересечению их множеств.
LaTeX
$$$$ \\uparrow (s \\wedge t) = (\\uparrow s) \\cap (\\uparrow t). $$$$
Lean4
@[simp, norm_cast]
theorem coe_inf : ∀ s t : Interval α, (↑(s ⊓ t) : Set α) = ↑s ∩ ↑t
| ⊥, _ => by
rw [bot_inf_eq]
exact (empty_inter _).symm
| (s : NonemptyInterval α), ⊥ => by
rw [inf_bot_eq]
exact (inter_empty _).symm
| (s : NonemptyInterval α), (t : NonemptyInterval α) =>
by
simp only [Min.min, coe_coe, NonemptyInterval.coe_def, Icc_inter_Icc, SemilatticeInf.inf, Lattice.inf]
split_ifs with h
· simp only [coe_coe, NonemptyInterval.coe_def]
· refine (Icc_eq_empty <| mt ?_ h).symm
exact fun h ↦ ⟨le_sup_left.trans <| h.trans inf_le_right, le_sup_right.trans <| h.trans inf_le_left⟩
