English
Let ι1, ι2, α be types with ι2 preordered and α a complete lattice. For an Antitone f: ι2 → α and a φ: ι1 → ι2 with Tendsto φ l atBot, then ⨆ i, f i = ⨆ i, f(φ i).
Русский
Пусть ι1, ι2, α — типы, ι2 упорядочен, α — полная решетка. Для антимонотонной f: ι2 → α и φ: ι1 → ι2 с Tendsto φ l atBot верно: ⨆ i, f i = ⨆ i, f(φ i).
LaTeX
$$$\text{Antitone}(f) \land \text{Tendsto}(\phi, l, \text{atBot}) \Rightarrow \bigvee_{i} f(i) = \bigvee_{i} f(\phi(i))$$$
Lean4
theorem iSup_eq_iSup_subseq_of_antitone {ι₁ ι₂ α : Type*} [Preorder ι₂] [CompleteLattice α] {l : Filter ι₁} [l.NeBot]
{f : ι₂ → α} {φ : ι₁ → ι₂} (hf : Antitone f) (hφ : Tendsto φ l atBot) : ⨆ i, f i = ⨆ i, f (φ i) :=
le_antisymm
(iSup_mono' fun i => Exists.imp (fun j (hj : φ j ≤ i) => hf hj) (hφ.eventually <| eventually_le_atBot i).exists)
(iSup_mono' fun i => ⟨φ i, le_rfl⟩)
