English
IsNormal is characterized by strict monotonicity and a successor-limit condition: IsNormal f iff f is strictly monotone and for every successor-limit o and every a, if f b ≤ a for all b < o, then f o ≤ a.
Русский
IsNormal задаётся как строгая монотонность и условие предшественника-предела: IsNormal f эквивалентно тому, что f строго монотонна и для каждого o, являющегося пределом-соседом, и для каждого a, если для всех b < o выполнено f b ≤ a, то f o ≤ a.
LaTeX
$$$\text{IsNormal}(f) \iff \Big( \text{StrictMono}(f) \land \forall o\, \text{IsSuccLimit}(o) \to \forall a\, (\forall b < o, f b \le a) \to f o \le a \Big)$$$
Lean4
theorem isNormal_iff [LinearOrder α] [LinearOrder β] {f : α → β} :
IsNormal f ↔ StrictMono f ∧ ∀ o, IsSuccLimit o → ∀ a, (∀ b < o, f b ≤ a) → f o ≤ a := by
simp [isNormal_iff', mem_lowerBounds, mem_upperBounds]
