English
The set underlying the infimum of a family of intervals equals the iterated intersection of their carrier sets.
Русский
Множество, соответствующее Infimum семейства интервалов, равно итеративному пересечению их множеств.
LaTeX
$$$$ ↑(\\mathrm{sInf}\\; S) = \\bigcap_{s \\in S} (s : Set \\alpha). $$$$
Lean4
@[simp, norm_cast]
theorem coe_sInf [DecidableLE α] (S : Set (Interval α)) : ↑(sInf S) = ⋂ s ∈ S, (s : Set α) := by
classical
change ((dite _ _ _ : Interval α) : Set α) = ⋂ (s : Interval α) (_ : s ∈ S), (s : Set α)
split_ifs with h
· ext
simp [Interval.forall, h.1, ← forall_and, ← NonemptyInterval.mem_def]
simp_rw [not_and_or, Classical.not_not] at h
rcases h with h | h
· refine (eq_empty_of_subset_empty ?_).symm
exact iInter₂_subset_of_subset _ h Subset.rfl
· refine (not_nonempty_iff_eq_empty.1 ?_).symm
rintro ⟨x, hx⟩
rw [mem_iInter₂] at hx
exact h fun s ha t hb => (hx _ ha).1.trans (hx _ hb).2
