subtype_map — Mathlib

English

If f is continuous and hpq relates p to q via f, then Subtype.map f hpq is continuous.

Русский

Если f непрерывно, и hpq устанавливает связь p к q через f, то Subtype.map f hpq непрерывно.

LaTeX

$$$\text{Continuous}(f) \rightarrow (\forall x, p x \rightarrow q(f x)) \rightarrow \text{Continuous}(\text{Subtype.map } f hpq)$$$

Lean4

@[fun_prop]
theorem subtype_map {f : X → Y} (h : Continuous f) {q : Y → Prop} (hpq : ∀ x, p x → q (f x)) :
    Continuous (Subtype.map f hpq) :=
  (h.comp continuous_subtype_val).subtype_mk _

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