restr_eqOn_source — Mathlib

English

EqOnSource is definitional to PartialEquiv.EqOnSource via toPartialEquiv.

Русский

EqOnSource эквивалентно PartialEquiv.EqOnSource через toPartialEquiv по определению.

LaTeX

$$$ EqOnSource(e,e') \iff PartialEquiv.EqOnSource\left(e.toPartialEquiv, e'.toPartialEquiv\right) $$$

Lean4

/-- Two equivalent open partial homeomorphisms are equal when the source and target are `univ`. -/
theorem restr_eqOn_source {e e' : OpenPartialHomeomorph X Y} (h : EqOn e e' (e.source ∩ e'.source)) :
    e.restr e'.source ≈ e'.restr e.source := by
  constructor
  · rw [e'.restr_source' _ e.open_source]
    rw [e.restr_source' _ e'.open_source]
    exact Set.inter_comm _ _
  · rw [e.restr_source' _ e'.open_source]
    refine (EqOn.trans ?_ h).trans ?_ <;> simp only [mfld_simps, eqOn_refl]

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