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