sInf_prod — Mathlib

English

Let α and β be InfSet spaces and s ⊆ α, t ⊆ β be nonempty. Then the infimum of the product set s ×ˢ t is the pair of infima: sInf (s ×ˢ t) = (sInf s, sInf t).

Русский

Пусть α и β — инфинитные множества, s ⊆ α, t ⊆ β непусты. Тогда наименьшее верхнее множество множества s × t это пара (sInf s, sInf t).

LaTeX

$$$ sInf (s \timesˢ t) = (sInf s, sInf t) $$$

Lean4

theorem sInf_prod [InfSet α] [InfSet β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) :
    sInf (s ×ˢ t) = (sInf s, sInf t) :=
  congr_arg₂ Prod.mk (congr_arg sInf <| fst_image_prod _ ht) (congr_arg sInf <| snd_image_prod hs _)

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