English
Let s be a finite set of indices and f: ι → α. Then a < ⨅ i∈s f(i) if and only if a < f(x) for every x ∈ s.
Русский
Пусть s—конечное множество индексов и f: ι → α. Тогда a < ⨅ i∈s f(i) тогда и только если a < f(x) для каждого x ∈ s.
LaTeX
$$$a < \inf_{i∈s} f(i) \iff ∀ x∈s, a < f(x).$$$
Lean4
theorem lt_ciInf_iff {s : Set ι} {f : ι → α} (hs : s.Finite) (h : ∃ x ∈ s, f x ≤ sInf ∅) :
a < ⨅ i ∈ s, f i ↔ ∀ x ∈ s, a < f x := by
constructor
· intro h x hx
refine h.trans_le (csInf_le ?_ ?_)
·
classical
refine (((hs.image f).union (finite_singleton (sInf ∅))).subset ?_).bddBelow
intro
simp only [ciInf_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image, forall_exists_index]
grind
· simp only [mem_range]
refine ⟨x, ?_⟩
simp [hx]
· intro H
have := hs.ciInf_mem_image _ h
simp only [mem_image] at this
obtain ⟨_, hmem, hx⟩ := this
rw [← hx]
exact H _ hmem
