restr_eqOnSource_restr — Mathlib

English

Two equivalent open partial homeomorphisms remain equivalent when restricted to different interiors, provided the interior intersections coincide.

Русский

Два эквивалентных открытых частичных гомеоморфизма сохраняют эквивалентность при ограничении к разным interior, если их пересечения interior совпадают.

LaTeX

$$$ e.restr s \approx e'.restr s' \text{ when } e.source \cap interior s = e.source \cap interior s' $$$

Lean4

theorem restr_eqOnSource_restr {s' : Set X} (hss' : e.source ∩ interior s = e.source ∩ interior s') :
    e.restr s ≈ e.restr s' := by
  constructor
  · simpa [e.restr_source]
  · simp [Set.eqOn_refl]

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