mono_pre_nat — Mathlib

English

mkMetric'(m) equals the iSup of its pre m over n⁻¹; i.e., mkMetric'(m) = ⨆ n, mkMetric'.pre m n⁻¹.

Русский

mkMetric'(m) равен наивысшему верхнему пределу (iSup) по предела m над n⁻¹: mkMetric'(m) = ⨆ n mkMetric'.pre m n⁻¹.

LaTeX

$$$\\mathrm{mkMetric'}(m) = \\bigsqcup_{n \\in \\mathbb{N}} \\mathrm{mkMetric}'.\\mathrm{pre}\\, m\, n^{-1}$$$

Lean4

theorem mono_pre_nat (m : Set X → ℝ≥0∞) : Monotone fun k : ℕ => pre m k⁻¹ := fun k l h =>
  le_pre.2 fun _ hs => pre_le (hs.trans <| by simpa)

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