Theorems · Theorem · general topology

PartialEquiv.image_source_inter_eq

∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α),
  ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)

Defined in

Mathlib.Logic.Equiv.PartialEquiv

Cited by

3 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound