monotone_preimage — Mathlib

English

The map s ↦ preimage(s, f) is monotone with respect to inclusion: if s ⊆ t then preimage(s) ⊆ preimage(t).

Русский

Отображение s ↦ preimage(s, f) монотонно по включению: если s ⊆ t, то предобраз s ⊆ предобраз t.

LaTeX

$$$$ s \\subseteq t \\Rightarrow \\mathrm{preimage}(s,f) \\subseteq \\mathrm{preimage}(t,f). $$$$

Lean4

theorem monotone_preimage {f : α → β} (h : Injective f) : Monotone fun s => preimage s f h.injOn := fun _ _ H _ hx =>
  mem_preimage.2 (H <| mem_preimage.1 hx)

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