snd_surjective — Mathlib

English

If α is nonempty, the second projection snd: α × β → β is surjective.

Русский

Если α непусто, проекция snd: α × β → β сюръективна.

LaTeX

$$$[h : Nonempty \\\\alpha] \\\\Rightarrow \\\\operatorname{Surjective}(\\\\operatorname{snd}) \\\\text{, i.e. } \\\\forall b \\\\in \\\\beta, \\\\exists a \\\\in \\\\alpha, \\\\operatorname{snd}(a,b) = b.$$$

Lean4

theorem snd_surjective [h : Nonempty α] : Function.Surjective (@snd α β) := fun y ↦ h.elim fun x ↦ ⟨⟨x, y⟩, rfl⟩

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