bsup_le_iff — Mathlib

English

A strengthened bound: lifting the card of sInf of sᶜ is bounded by the cardinality of s.

Русский

Усиленная граница: подъем кардинала sInf sᶜ ограничен кардиналом s.

LaTeX

$$$$ \\operatorname{lift}( (\\operatorname{sInf}(s^{c})) . \\operatorname{card} ) \\le \\#s $$$$

Lean4

theorem bsup_le_iff {o f a} : bsup.{u, v} o f ≤ a ↔ ∀ i h, f i h ≤ a :=
  Ordinal.iSup_le_iff.trans
    ⟨fun h i hi => by
      rw [← familyOfBFamily_enum o f]
      exact h _, fun h _ => h _ _⟩

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