lt_iff_exists_lt — Mathlib

English

For IsNormal f in a dual setting, f a ≤ b is equivalent to a' < a implies f a' ≤ b.

Русский

Для IsNormal f в двойственном контексте: f(a) ≤ b тогда и только тогда, когда для всех a' < a выполняется f(a') ≤ b.

LaTeX

$$$f\,a \le b \iff \forall a' < a,\ f(a') \le b$$$

Lean4

theorem lt_iff_exists_lt (hf : IsNormal f) (ha : IsSuccLimit a) {b : β} : b < f a ↔ ∃ a' < a, b < f a' := by
  simpa [mem_upperBounds] using lt_isLUB_iff (hf.isLUB_image_Iio_of_isSuccLimit ha)

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