isNormal

Mathlib.Order.IsNormal

URI: https://scilib.ai/kg/mathlib#InitialSeg.isNormal

← MathLib Explorer

English

If f is an InitialSeg, then f is IsNormal.

Русский

Если f является InitialSeg, то она IsNormal.

LaTeX

$$$\IsNormal(f)$$$

Lean4

theorem _root_.InitialSeg.isNormal (f : α ≤i β) : IsNormal f
    where
  strictMono := f.strictMono
  mem_lowerBounds_upperBounds_of_isSuccLimit
    ha := by
    rw [f.image_Iio]
    exact (f.map_isSuccLimit ha).isLUB_Iio.2

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru