apply_le_nfpFamily — Mathlib

English

If H i: IsNormal (f i), then (∀ i, f i b) ≤ nfpFamily f a iff b ≤ nfpFamily f a.

Русский

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

LaTeX

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

Lean4

theorem apply_le_nfpFamily [Small.{u} ι] [hι : Nonempty ι] (H : ∀ i, IsNormal (f i)) {a b} :
    (∀ i, f i b ≤ nfpFamily f a) ↔ b ≤ nfpFamily f a :=
  by
  refine ⟨fun h => ?_, fun h i => ?_⟩
  · obtain ⟨i⟩ := hι
    exact (H i).le_apply.trans (h i)
  · rw [← nfpFamily_fp (H i)]
    exact (H i).monotone h

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