Theorems · Theorem · general topology
Homeomorph.image_interior
∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (s : Set X),
⇑h '' interior s = interior (⇑h '' s)- Defined in
- Mathlib.Topology.Homeomorph.Defs
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Set.imagestatement · cited by 5,609
- Set.preimageproof · cited by 4,946
- Homeomorphstatement and proof · cited by 725
- interiorstatement and proof · cited by 714
- Homeomorph.symmproof · cited by 365
- Homeomorph.preimage_symmproof · cited by 9
- Homeomorph.preimage_interiorproof · cited by 2
Cited by5
Results whose statement or proof uses this declaration.
- interior_vaddproof · cited by 3
- interior_smul₀proof · cited by 2
- IsHomeomorph.image_interiorproof · cited by 1
- Real.Convex.dimH_eq_finrank_vectorSpanproof · cited by 1
- interior_smulproof · cited by 1