snd_bot — Mathlib

English

The second projection of the bottom element of the product is the bottom of the second factor: snd(⊥α×β) = ⊥β.

Русский

Вторая проекция нижнего элемента произведения равна нижнему элементу второй компоненты: snd(⊥α×β) = ⊥β.

LaTeX

$$$\\operatorname{snd}(\\bot_{\\alpha\\times\\beta}) = \\bot_{\\beta}$$$

Lean4

@[simp]
theorem snd_bot [Bot α] [Bot β] : (⊥ : α × β).snd = ⊥ :=
  rfl

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