English
Equality of the symmetric-transformed subtypeRestr maps when U ≤ V and Nonempty subtypes hold, expressed as EqOn with Function composition by Set.inclusion.
Русский
Равенство симметризированных ограничений subtypeRestr при U ≤ V и существовании подтипов выражено как EqOn с композицией по Set.inclusion.
LaTeX
$$$ {U V : Opens X} (hU : Nonempty U) (hV : Nonempty V) (hUV : U ≤ V) : EqOn (e.subtypeRestr hV).symm.toFun' (Function.comp (Set.inclusion hUV) (e.subtypeRestr hU).symm.toFun') (e.subtypeRestr hU).target $$$
Lean4
/-- This lemma characterizes the transition functions of an open subset in terms of the transition
functions of the original space. -/
theorem subtypeRestr_symm_trans_subtypeRestr (f f' : OpenPartialHomeomorph X Y) :
(f.subtypeRestr hs).symm.trans (f'.subtypeRestr hs) ≈ (f.symm.trans f').restr (f.target ∩ f.symm ⁻¹' s) :=
by
simp only [subtypeRestr_def, trans_symm_eq_symm_trans_symm]
have openness₁ : IsOpen (f.target ∩ f.symm ⁻¹' s) := f.isOpen_inter_preimage_symm s.2
rw [← ofSet_trans _ openness₁, ← trans_assoc, ← trans_assoc]
refine
EqOnSource.trans' ?_
(eqOnSource_refl _)
-- f' has been eliminated !!!
have set_identity : f.symm.source ∩ (f.target ∩ f.symm ⁻¹' s) = f.symm.source ∩ f.symm ⁻¹' s := by mfld_set_tac
have openness₂ : IsOpen (s : Set X) := s.2
rw [ofSet_trans', set_identity, ← trans_of_set' _ openness₂, trans_assoc]
refine
EqOnSource.trans' (eqOnSource_refl _)
?_
-- f has been eliminated !!!
refine Setoid.trans (symm_trans_self (s.openPartialHomeomorphSubtypeCoe hs)) ?_
simp only [mfld_simps, Setoid.refl]
