of_mem_lowerBounds_upperBounds — Mathlib

English

An initial-segment map that respects order into a linear order is normal.

Русский

У отображения типа InitialSeg, сохраняющего порядок, линейного порядка, нормальная функция.

LaTeX

$$$\text{IsNormal}(f)$$$

Lean4

@[deprecated "use the default constructor of `IsNormal` directly" (since := "2025-07-08")]
theorem of_mem_lowerBounds_upperBounds {f : α → β} (hf : StrictMono f)
    (hl : ∀ {a}, IsSuccLimit a → f a ∈ lowerBounds (upperBounds (f '' Iio a))) : IsNormal f :=
  ⟨hf, hl⟩

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