lfpApprox_monotone — Mathlib

English

The fixed-point approximation lfpApprox assembled from a monotone order-preserving map is monotone with respect to the ordinal index.

Русский

Аппроксимация наименьшей точки фиксированности (lfpApprox), построенная из монотонного отображения, неискажимо монотонна по индексу ординала.

LaTeX

$$$ \\text{Monotone}(\\mathrm{lfpApprox}\, f\, x) $$$

Lean4

theorem lfpApprox_monotone : Monotone (lfpApprox f x) :=
  by
  intro a b h
  rw [lfpApprox, lfpApprox]
  gcongr sSup (?_ ∪ { x })
  simp only [exists_prop, Set.setOf_subset_setOf, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
  intro a' h'
  use a'
  exact ⟨lt_of_lt_of_le h' h, rfl⟩

Похожие утверждения