image_strictMono — Mathlib

English

If f is injective, the map s ↦ f''s is strictly monotone with respect to inclusion: s ⊂ t implies f''s ⊂ f''t.

Русский

Если f инъективно, отображение s ↦ f''s строго монотонно по включению: s ⊂ t тогда и только тогда, что f''s ⊂ f''t.

LaTeX

$$$s \subsetneq t \Rightarrow f''s \subsetneq f''t\quad\text{при } f\text{ инъективном}.$$$

Lean4

theorem image_strictMono (inj : Function.Injective f) : StrictMono (image f) :=
  monotone_image.strictMono_of_injective inj.image_injective

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