IsInteger — Mathlib

English

IsInteger f x is defined to mean that x lies in the range of the localization map f.

Русский

IsInteger f x определяется как то, что x лежит в образе локализационного отображения f.

LaTeX

$$$\operatorname{IsInteger}(f,x) \iff x \in \operatorname{Range}(f)$$$

Lean4

/-- Given `x : M'`, `M'` a localization of `M` via `f`, `IsInteger f x` iff `x` is in the image of
the localization map `f`. -/
def IsInteger (x : M') : Prop :=
  x ∈ LinearMap.range f

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