Image transport for compositions and restrictions of partial equivalences

This file supplements PartialEquiv.image_source_inter_eq' and PartialEquiv.image_trans_source in Mathlib.Logic.Equiv.PartialEquiv with equational formulas for source-restricted images under compositions e.trans e', source restrictions e.restr u, and coordinate transitions e.symm.trans e' (with or without restriction to a subset u of the intermediate space).

Main declarations

• PartialEquiv.image_trans_source_inter: (e.trans e') '' ((e.trans e').source ∩ s) = e' '' (e'.source ∩ e '' (e.source ∩ s)).
• PartialEquiv.image_restr_source_inter: (e.restr u) '' ((e.restr u).source ∩ s) = (e.restr u).target ∩ e '' (e.source ∩ s).
• PartialEquiv.image_symm_trans_source_inter and PartialEquiv.image_restr_symm_trans_source_inter: transport of e '' (e.source ∩ s) onto e' '' (e'.source ∩ s) intersected with the transition target.
• PartialEquiv.preimage_eq_iUnion_symm_image: if every point of f ⁻¹' P lies in the source of one of a family of partial equivalences e x, the preimage is the union of the images under (e x).symm of the sets of coordinates which f ∘ (e x).symm carries into P.

theorem PartialEquiv.image_trans_source_inter {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) (s : Set α) : ↑(e.trans e') '' ((e.trans e').source ∩ s) = ↑e' '' (e'.source ∩ ↑e '' (e.source ∩ s))

Pushing a set forward along a composition e.trans e' of partial equivalences pushes its e-source trace through e and then its e'-source trace through e'.

theorem PartialEquiv.image_restr_source_inter {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (u s : Set α) : ↑(e.restr u) '' ((e.restr u).source ∩ s) = (e.restr u).target ∩ ↑e '' (e.source ∩ s)

Restricting a partial equivalence to u intersects source-restricted images with the restricted target.

theorem PartialEquiv.image_symm_trans_source_inter {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv α γ) (s : Set α) : ↑(e.symm.trans e') '' ((e.symm.trans e').source ∩ ↑e '' (e.source ∩ s)) = (e.symm.trans e').target ∩ ↑e' '' (e'.source ∩ s)

A transition partial equivalence e.symm.trans e' transports the e-image of s onto the part of the e'-image of s lying in (e.symm.trans e').target.

theorem PartialEquiv.image_restr_symm_trans_source_inter {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv α γ) (u : Set β) (s : Set α) : ↑((e.symm.trans e').restr u) '' (((e.symm.trans e').restr u).source ∩ ↑e '' (e.source ∩ s)) = ((e.symm.trans e').restr u).target ∩ ↑e' '' (e'.source ∩ s)

Restricting a transition partial equivalence e.symm.trans e' to u ⊆ β transports the e-image of s onto the part of the e'-image of s lying in ((e.symm.trans e').restr u).target.

theorem PartialEquiv.preimage_eq_iUnion_symm_image {α : Type u_1} {β : Type u_2} {ι : Type u_4} {δ : Type u_5} {f : α → δ} {e : ι → PartialEquiv α β} {P : Set δ} {T : ι → Set β} (hT : ∀ (x : ι), T x ⊆ (e x).target) (hiff : ∀ (x : ι), ∀ w ∈ (e x).target, w ∈ T x ↔ f (↑(e x).symm w) ∈ P) (hfull : ∀ (z : α), f z ∈ P → z ∈ ⋃ (x : ι), (e x).source) : f ⁻¹' P = ⋃ (x : ι), ↑(e x).symm '' T x

A preimage as a union of chart images. Let e x be partial equivalences with T x ⊆ (e x).target such that a coordinate w ∈ (e x).target lies in T x exactly when its image under f ∘ (e x).symm lies in P. If every point of f ⁻¹' P lies in some source (e x).source, then f ⁻¹' P is the union of the sets (e x).symm '' T x.