srange_fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem srange_fst [Nonempty N] : (fst M N).srange = ⊤ :=
  (fst M N).srange_eq_top_of_surjective <| Prod.fst_surjective

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