mono — Mathlib

English

If a local homeomorph on a larger set holds, it remains on any subset.

Русский

Если локальный гомеоморфизм на большем множестве существует, он сохраняется на любом подмножестве.

LaTeX

$$$IsLocalHomeomorphOn\\, f\\, t \\Rightarrow s\\subseteq t \\Rightarrow IsLocalHomeomorphOn\\, f\\, s$$$

Lean4

theorem mono {t : Set X} (hf : IsLocalHomeomorphOn f t) (hst : s ⊆ t) : IsLocalHomeomorphOn f s := fun x hx ↦
  hf x (hst hx)

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