nfpFamily_le_fp — Mathlib

English

If H i: IsNormal (f i) for all i, and for all i, f i b ≤ b, then nfpFamily f a ≤ b provided a ≤ b and H monotone control.

Русский

Если для всех i функция f_i нормальная, и для всех i выполняется f_i(b) ≤ b, тогда при a ≤ b имеем nfpFamily f a ≤ b.

LaTeX

$$$[Small.{u} ι] [H : \\forall i, Monotone (f i)] {a b} (ab : a \\le b) (h : \\forall i, f i b \\le b) : nfpFamily f a \\le b$$

Lean4

theorem nfpFamily_le_fp (H : ∀ i, Monotone (f i)) {a b} (ab : a ≤ b) (h : ∀ i, f i b ≤ b) : nfpFamily f a ≤ b :=
  by
  apply Ordinal.iSup_le fun l ↦ ?_
  induction l generalizing a with
  | nil => exact ab
  | cons i l IH => exact (H i (IH ab)).trans (h i)

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