mem_range_lift_of_le

Mathlib.SetTheory.Cardinal.Order

URI: https://scilib.ai/kg/mathlib#Cardinal.mem_range_lift_of_le

← MathLib Explorer

English

If b ≤ lift a, then b lies in the range of lift.

Русский

Если b ≤ lift a, тогда b принадлежит образу lift.

LaTeX

$$$$ b \\le \\mathrm{lift}(a) \\Rightarrow b \\in \\mathrm{range}(\\mathrm{lift}). $$$$

Lean4

theorem mem_range_lift_of_le {a : Cardinal.{u}} {b : Cardinal.{max u v}} :
    b ≤ lift.{v, u} a → b ∈ Set.range lift.{v, u} :=
  liftInitialSeg.mem_range_of_le

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

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

Разделы

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

Аффилиация

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