English
A general version of image supremum for indexed families, with dualization to obtain equality between a two-step supremum and a direct supremum.
Русский
Обобщенная версия верхней грани образа для индексированных семей; равенство между двухступенчатым верхним пределом и прямым верхним пределом.
LaTeX
$$$\left( \sup_{i} g(f(i)) \right) = \left( \sup_{x} g(x) \right) \text{ under suitable bounds}.$$$
Lean4
theorem ciSup_image {α ι ι' : Type*} [ConditionallyCompleteLattice α] [Nonempty ι] [Nonempty ι'] {s : Set ι}
(hs : s.Nonempty) {f : ι → ι'} {g : ι' → α} (hf : BddAbove (Set.range fun i : s ↦ g (f i)))
(hg' : sSup ∅ ≤ ⨆ i : s, g (f i)) : ⨆ i ∈ (f '' s), g i = ⨆ x ∈ s, g (f x) :=
by
have hg : BddAbove (Set.range fun i : f '' s ↦ g i) := by simpa [bddAbove_def] using hf
have hf' : sSup ∅ ≤ ⨆ i : f '' s, g i := by
refine hg'.trans ?_
have : Nonempty s := Set.Nonempty.to_subtype hs
refine ciSup_le ?_
intro ⟨i, h⟩
obtain ⟨t, ht⟩ : ∃ t : f '' s, g t = g (f (Subtype.mk i h)) :=
by
have : f i ∈ f '' s := Set.mem_image_of_mem _ h
exact ⟨⟨f i, this⟩, by simp⟩
rw [← ht]
refine le_ciSup_set ?_ t.prop
simpa [bddAbove_def] using hf
rw [← csSup_image (by simpa using hs) hg hf', ← csSup_image hs hf hg', ← Set.image_comp, comp_def]
