English
An element of the atlas yields an open partial homeomorphism between M and H for the topology generated by the atlas.
Русский
Элемент атласа задаёт открытое частичное гомоморфизм между M и H в топологии атласа.
LaTeX
$$$\text{openPartialHomeomorph}(e,he) : \text{OpenPartialHomeomorph } M H$ for $e\in atlas(H,M)$.$$
Lean4
/-- An element of the atlas in a charted space without topology becomes an open partial
homeomorphism for the topology constructed from this atlas. The `OpenPartialHomeomorph` version is
given in this definition. -/
protected def openPartialHomeomorph (e : PartialEquiv M H) (he : e ∈ c.atlas) :
@OpenPartialHomeomorph M H c.toTopologicalSpace _ :=
{ __ := c.toTopologicalSpace
__ := e
open_source := by convert c.open_source' he
open_target := by convert c.open_target he
continuousOn_toFun := by
letI : TopologicalSpace M := c.toTopologicalSpace
rw [continuousOn_open_iff (c.open_source' he)]
intro s s_open
rw [inter_comm]
apply TopologicalSpace.GenerateOpen.basic
simp only [exists_prop, mem_iUnion, mem_singleton_iff]
exact ⟨e, he, ⟨s, s_open, rfl⟩⟩
continuousOn_invFun := by
letI : TopologicalSpace M := c.toTopologicalSpace
apply continuousOn_isOpen_of_generateFrom
intro t ht
simp only [exists_prop, mem_iUnion, mem_singleton_iff] at ht
rcases ht with ⟨e', e'_atlas, s, s_open, ts⟩
rw [ts]
let f := e.symm.trans e'
have : IsOpen (f ⁻¹' s ∩ f.source) := by
simpa [f, inter_comm] using
(continuousOn_open_iff (c.open_source e e' he e'_atlas)).1 (c.continuousOn_toFun e e' he e'_atlas) s s_open
have A :
e' ∘ e.symm ⁻¹' s ∩ (e.target ∩ e.symm ⁻¹' e'.source) = e.target ∩ (e' ∘ e.symm ⁻¹' s ∩ e.symm ⁻¹' e'.source) :=
by
rw [← inter_assoc, ← inter_assoc]
congr 1
exact inter_comm _ _
simpa [f, PartialEquiv.trans_source, preimage_inter, preimage_comp.symm, A] using this }
