prod_map_atBot_eq — Mathlib

English

The dual statement to prod_map_atTop_eq, relating maps of atBot and a product map under dual orders.

Русский

Дуальная версия утверждения prod_map_atTop_eq, касающаяся отображения atBot и произведения по двойному порядку.

LaTeX

$$$\\operatorname{SProd.sprod}(\\operatorname{map} u_1\\, \\operatorname{atBot})\\, (\\operatorname{map} u_2\\, \\operatorname{atBot}) = \\operatorname{map}(\\operatorname{Prod.map} u_1\\, u_2)\\, \\operatorname{atBot}$$$

Lean4

theorem prod_map_atBot_eq {α₁ α₂ β₁ β₂ : Type*} [Preorder β₁] [Preorder β₂] (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) :
    map u₁ atBot ×ˢ map u₂ atBot = map (Prod.map u₁ u₂) atBot :=
  @prod_map_atTop_eq _ _ β₁ᵒᵈ β₂ᵒᵈ _ _ _ _

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