lt_bsup_of_ne_bsup — Mathlib

English

Let o and a family f be as above. The statement says a condition on all i,h: either f(i,h) ≠ bsup o f or f(i,h) < bsup o f. Equivalently, the negation of all f(i,h) ≥ bsup o f is equivalent to all f(i,h) < bsup o f.

Русский

Пусть имеется o и семейство f. Тогда для всех i, hi: f(i, hi) ≠ bsup o f эквивалентно f(i, hi) < bsup o f.

LaTeX

$$$(\\forall i\\, h, f(i,h) \\neq \\operatorname{bsup}(o, f)) \\iff (\\forall i\\, h, f(i,h) < \\operatorname{bsup}(o, f))$$$

Lean4

theorem lt_bsup_of_ne_bsup {o : Ordinal.{u}} {f : ∀ a < o, Ordinal.{max u v}} :
    (∀ i h, f i h ≠ bsup.{_, v} o f) ↔ ∀ i h, f i h < bsup.{_, v} o f :=
  ⟨fun hf _ _ => lt_of_le_of_ne (le_bsup _ _ _) (hf _ _), fun hf _ _ => ne_of_lt (hf _ _)⟩

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