univLE_total

Mathlib.SetTheory.Cardinal.UnivLE

URI: https://scilib.ai/kg/mathlib#univLE_total

← MathLib Explorer

English

For any universe levels u and v, either UnivLE(u,v) or UnivLE(v,u) holds.

Русский

Для любых уровней вселенных u и v либо UnivLE(u,v), либо UnivLE(v,u) выполняются.

LaTeX

$$$ UnivLE(u,v) \\lor UnivLE(v,u) $$$

Lean4

/-- Together with transitivity, this shows `UnivLE` is a total preorder. -/
theorem univLE_total : UnivLE.{u, v} ∨ UnivLE.{v, u} := by simp_rw [univLE_iff_cardinal_le]; apply le_total

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

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

Разделы

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

Аффилиация

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