down_sInf — Mathlib

English

For InfSet α, the down projection commutes with sInf: the down of the infimum of a set of ULift α equals the infimum of the preimage under ULift.up.

Русский

Для InfSet α спускается через ULift: понижениеInf множества ULift α равно инфинуму прообразов.

LaTeX

$$$\downarrow(\mathrm{sInf}\ s) = \mathrm{sInf}(ULift.up^{-1}(s))$$$

Lean4

theorem down_sInf [InfSet α] (s : Set (ULift.{v} α)) : (sInf s).down = sInf (ULift.up ⁻¹' s) :=
  rfl

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