preimage_val — Mathlib

English

If t is open, then the preimage under the inclusion map of t is open in the subspace.

Русский

Если t открыто, то предобраз через включение является открытым в подпространстве.

LaTeX

$$$\\forall X,\\; \\text{IsOpen}(t) \\Rightarrow \\text{IsOpen}\\left(\\text{preimage}\\;\\text{Subtype.val } t\\right).$$$

Lean4

theorem preimage_val {s t : Set X} (ht : IsOpen t) : IsOpen (s ↓∩ t) :=
  ht.preimage continuous_subtype_val

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