map_strictMono_of_injective — Mathlib

English

Let M and N be monoids and f: M → N a monoid hom with f injective. Then the map S ↦ f[S] from Submonoid M to Submonoid N is strictly monotone with respect to inclusion; equivalently, if S ⊊ T then f[S] ⊊ f[T].

Русский

Пусть M и N — моноиды, f: M → N моноид-гомоморфизм с инъекцией. Отображение S ↦ f[S] между подмоноидами M строго монотонно по включению; то есть S ⊊ T ⇒ f[S] ⊊ f[T].

LaTeX

$$$ \operatorname{Injective}(f) \Rightarrow \operatorname{StrictMono}\big(\operatorname{map} f\big). $$$

Lean4

@[to_additive]
theorem map_strictMono_of_injective : StrictMono (map f) :=
  (gciMapComap hf).strictMono_l

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