English
If s and s' are open subsets of X, then composing the open partial homeomorphisms ofSet s hs and ofSet s' hs' yields the open partial homeomorphism ofSet (s ∩ s') IsOpen.inter hs hs'.
Русский
Если s и s' — открытые подмножества X, то композиция OpenPartialHomeomorph.ofSet s hs и OpenPartialHomeomorph ofSet s' hs' равна OpenPartialHomeomorph.ofSet (s ∩ s') (IsOpen.inter hs hs').
LaTeX
$$$ (OpenPartialHomeomorph.ofSet s hs).trans (OpenPartialHomeomorph.ofSet s' hs') = OpenPartialHomeomorph.ofSet (s \cap s') (IsOpen.inter hs hs') $$$
Lean4
@[simp, mfld_simps]
theorem ofSet_trans_ofSet {s : Set X} (hs : IsOpen s) {s' : Set X} (hs' : IsOpen s') :
(ofSet s hs).trans (ofSet s' hs') = ofSet (s ∩ s') (IsOpen.inter hs hs') :=
by
rw [(ofSet s hs).trans_ofSet hs']
ext <;> simp [hs'.interior_eq]
