nfpFamily_le_apply — Mathlib

English

If Nonempty ι and Small ι with H, then (exists i, nfpFamily f a ≤ f i b) ↔ nfpFamily f a ≤ b.

Русский

Если существует i такой, что nfpFamily f a ≤ f i b, тогда и только тогда nfpFamily f a ≤ b при условии H.

LaTeX

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

Lean4

theorem nfpFamily_le_apply [Nonempty ι] [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a b} :
    (∃ i, nfpFamily f a ≤ f i b) ↔ nfpFamily f a ≤ b :=
  by
  rw [← not_iff_not]
  push_neg
  exact apply_lt_nfpFamily_iff H

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