of_le

Mathlib.SetTheory.Cardinal.HasCardinalLT

URI: https://scilib.ai/kg/mathlib#HasCardinalLT.of_le

English

If HasCardinalLT X κ and κ ≤ κ', then HasCardinalLT X κ'.

Русский

Если HasCardinalLT X κ и κ ≤ κ', то HasCardinalLT X κ'.

LaTeX

$$HasCardinalLT X κ → κ ≤ κ' → HasCardinalLT X κ'$$

Lean4

theorem of_le {κ' : Cardinal.{v}} (hκ' : κ ≤ κ') : HasCardinalLT X κ' :=
  lt_of_lt_of_le h (by simpa only [Cardinal.lift_le] using hκ')

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

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

Разделы

Аффилиация

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