finite_srange — Mathlib

English

If the domain R is finite, then the range of any morphism f : F is finite (as a subtype).

Русский

Если область определения R конечна, то образ отображения f — конечно (как подтип).

LaTeX

$$$ [Finite \; R] \rightarrow Finite (Subtype (\lambda x. x \in srange f)) $$$

Lean4

/-- The range of a morphism of non-unital semirings is finite if the domain is a finite. -/
instance finite_srange [Finite R] (f : F) : Finite (srange f : NonUnitalSubsemiring S) :=
  (Set.finite_range f).to_subtype

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