range_fst — Mathlib

English

The first projection fst: R×S → R and the second projection snd: R×S → S are surjective, i.e. their images are all of R and S, respectively.

Русский

Проекции fst и snd из произведения R×S на R и S естественным образом сюръективны: их изображения равны R и S.

LaTeX

$$$\mathrm{srange}(\text{fst }R,S)=\top$ and $\mathrm{srange}(\text{snd }R,S)=\top$$$

Lean4

theorem range_fst : NonUnitalRingHom.srange (fst R S) = ⊤ :=
  NonUnitalSubsemiring.range_fst

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