fintypeRange — Mathlib

English

If the domain A is finite and B has decidable equality, then the range (as a subtype) is finite.

Русский

Если область определения A конечна и B обладает разрешимостью равенств, то образ φ является конечным.

LaTeX

$$$[Fintype A] \; [DecidableEq B] \; (\varphi : A \to_R B) \Rightarrow Fintype(\varphi.range)$$

Lean4

/-- The range of a morphism of algebras is a fintype, if the domain is a fintype.

Note that this instance can cause a diamond with `Subtype.fintype` if `B` is also a fintype. -/
instance fintypeRange [Fintype A] [DecidableEq B] (φ : A →ₐ[R] B) : Fintype φ.range :=
  Set.fintypeRange φ

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