surjective — Mathlib

English

A multiplicative isomorphism is surjective; every element of N is the image of some element of M.

Русский

Мультипликативный изоморфизм сюръективен; каждый элемент N является образцом некоторого элемента M.

LaTeX

$$$\\text{MulEquiv}.surjective(e) : \\text{Surjective}(e)$$$

Lean4

@[to_additive]
protected theorem surjective (e : M ≃* N) : Function.Surjective e :=
  EquivLike.surjective e

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