lift_sInf — Mathlib

English

The lift of the infimum of a set of cardinals equals the infimum of the lifts of the set.

Русский

Перенос (лифтовое отображение) инфимума множества кардиналов равен инфимума перенесённого множества.

LaTeX

$$$\text{lift}(sInf\,s) = sInf\,(lift\,''\,s)$$$

Lean4

@[simp]
theorem lift_sInf (s : Set Cardinal) : lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s) :=
  by
  rcases eq_empty_or_nonempty s with (rfl | hs)
  · simp
  · exact lift_monotone.map_csInf hs

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