down_sSup — Mathlib

English

For any α with SupSet, the down projection commutes with sSup: the down of the supremum of a family of ULift α elements equals the supremum of the preimage under ULift.up.

Русский

Для любого α с SupSet, отображение вниз commute с sSup: понижение верхней грани множества ULift α даёт верхнюю границу соответствующей прообразной множества.

LaTeX

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

Lean4

theorem down_sSup [SupSet α] (s : Set (ULift.{v} α)) : (sSup s).down = sSup (ULift.up ⁻¹' s) :=
  rfl

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