snd_top — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem snd_top [Top α] [Top β] : (⊤ : α × β).snd = ⊤ :=
  rfl

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