up_sInf — Mathlib

English

Let α be a type with InfSet. For any subset s ⊆ α, the lift of the infimum of s equals the infimum (in the lifted world) of the preimage of s under the ULift-down map.

Русский

Пусть α имеет структуру InfSet. Для любого подмножества s ⊆ α справедливо, что поднятие инфимума s равно инфимума множества ULift α, состоящего из элементов, чьё.down принадлежит s, то есть preimage под ULift.down.

LaTeX

$$$\\mathrm{up}(\\inf s) = \\inf \\big( \\mathrm{down}^{-1}(s) \\big)$$$

Lean4

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

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