srange_snd — Mathlib

English

Let M, N, P be types with Mul; if M is nonempty, then the srange of snd from M × N to N is the top subsemigroup.

Русский

Пусть M, N, P — типы с умножением; если M непусто, то srange snd из M × N в N есть верхняя подполугруппа.

LaTeX

$$$[Nonempty\ M] \Rightarrow (\mathrm{snd}\ M\ N).srange = \top$$$

Lean4

@[to_additive (attr := simp)]
theorem srange_snd [Nonempty M] : (snd M N).srange = ⊤ :=
  (snd M N).srange_eq_top_of_surjective <| Prod.snd_surjective

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