apply_lt_nfpFamily_iff — Mathlib

English

Under Nonempty ι and Small ι with H, we have: (∀ i, f i b < nfpFamily f a) ↔ b < nfpFamily f a.

Русский

При условии Nonempty и Small ι с H имеем: (для всех i f i b < nfpFamily f a) эквивалентно b < nfpFamily f a.

LaTeX

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

Lean4

theorem apply_lt_nfpFamily_iff [Nonempty ι] [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a b} :
    (∀ i, f i b < nfpFamily f a) ↔ b < nfpFamily f a :=
  by
  refine ⟨fun h ↦ ?_, apply_lt_nfpFamily H⟩
  let ⟨l, hl⟩ := lt_nfpFamily_iff.1 (h (Classical.arbitrary ι))
  exact lt_nfpFamily_iff.2 <| ⟨l, (H _).le_apply.trans_lt hl⟩

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