English
If p ⊆ V is finite-dimensional and f maps p into p, then the restriction of f to p is injective iff it is surjective onto p.
Русский
Пусть p ⊆ V конечномерно; если f отображает p в p, то ограничение f на p инъективно тогда и только тогда сюръективно на p.
LaTeX
$$$\forall p: Subspace, [\operatorname{FiniteDimensional}_K p] \{f: V \to V\} (h: \forall x \in p, f x \in p) : \operatorname{InjOn} f p \iff \operatorname{SurjOn} f p p$$$
Lean4
theorem injOn_iff_surjOn {p : Submodule K V} [FiniteDimensional K p] {f : V →ₗ[K] V} (h : ∀ x ∈ p, f x ∈ p) :
Set.InjOn f p ↔ Set.SurjOn f p p :=
by
rw [Set.injOn_iff_injective, ← Set.MapsTo.restrict_surjective_iff h]
change Injective (f.domRestrict p) ↔ Surjective (f.restrict h)
simp [disjoint_iff, ← injective_iff_surjective]
