English
Let f be monotone on t, and s ⊆ t with the property that every y ∈ t has some x ∈ s with x ≤ y, and f''t is bounded below. Then the infimum of f''s equals the infimum of f''t.
Русский
Пусть f монотонна на t, s ⊆ t и для каждого y ∈ t существует x ∈ s такой, что x ≤ y, а f''t ограничено снизу. Тогда inf { f(x) : x ∈ s } = inf { f(x) : x ∈ t }.
LaTeX
$$$[Preorder\ \alpha][ConditionallyCompleteLattice\ \beta]\ {f:\alpha\to\beta}\; \Bigl( ht:\; BddBelow (f '' t) \Bigr) \Bigl( hf:\; MonotoneOn f t \Bigr) \Bigl( hst:\; s \subseteq t \Bigr) \Bigl( h:\; \forall y\in t,\ exists x\in s, x \le y \Bigr) :\ sInf (f '' s) = sInf (f '' t)$$$
Lean4
theorem csInf_eq_of_subset_of_forall_exists_le [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {s t : Set α}
(ht : BddBelow (f '' t)) (hf : MonotoneOn f t) (hst : s ⊆ t) (h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y) :
sInf (f '' s) = sInf (f '' t) := by
obtain rfl | hs := Set.eq_empty_or_nonempty s
· obtain rfl : t = ∅ := by simpa [Set.eq_empty_iff_forall_notMem] using h
rfl
refine le_antisymm ?_ (by gcongr; exacts [ht, hs.image f])
refine le_csInf ((hs.mono hst).image f) ?_
simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
intro a ha
obtain ⟨x, hxs, hxa⟩ := h a ha
exact csInf_le_of_le (ht.mono (image_mono hst)) ⟨x, hxs, rfl⟩ (hf (hst hxs) ha hxa)
