image_inf_product — Mathlib

English

The image of the product under uncurry of inf equals the infimum of images: image (uncurry (· ⊓ ·)) (s ×ˢ t) = s ⊼ t.

Русский

Образ произведения под uncurry инфимума равен инфимума изображений: image (uncurry (· ⊓ ·)) (s ×ˢ t) = s ⊼ t.

LaTeX

$$$ \operatorname{image}_{\text{uncurry}} (s \times^\! t) = s \⊼ t $$$

Lean4

theorem image_inf_product (s t : Finset α) : (s ×ˢ t).image (uncurry (· ⊓ ·)) = s ⊼ t :=
  image_uncurry_product _ _ _

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