apply_lt_nfpFamily — Mathlib

English

If each f_i is normal and hb: b < nfpFamily f a, then f_i b < nfpFamily f a for every i.

Русский

Если каждый f_i нормальны и hb: b < nfpFamily f a, то для каждого i имеем f_i b < nfpFamily f a.

LaTeX

$$$[Small\\;ι] (H : \\forall i, IsNormal (f i))\\; {a b} (hb : b < nfpFamily f a) (i) : f i b < nfpFamily f a$$$

Lean4

theorem apply_lt_nfpFamily [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a b} (hb : b < nfpFamily f a) (i) :
    f i b < nfpFamily f a :=
  let ⟨l, hl⟩ := lt_nfpFamily_iff.1 hb
  lt_nfpFamily_iff.2 ⟨i :: l, (H i).strictMono hl⟩

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