restrOpen_source — Mathlib

English

The source of the restricted open partial homeomorphism equals the intersection of the original source with s.

Русский

Область определения ограниченного открытого частичного гомоморфизма равна пересечению исходной области определения и s.

LaTeX

$$$(e.restrOpen s hs).source = e.source \\cap s$$$

Lean4

theorem restrOpen_source (s : Set X) (hs : IsOpen s) : (e.restrOpen s hs).source = e.source ∩ s :=
  rfl

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