Theorems · Theorem · general topology
induced_generateFrom_eq
∀ {α : Type u_1} {β : Type u_2} {b : Set (Set β)} {f : α → β},
TopologicalSpace.induced f (TopologicalSpace.generateFrom b) = TopologicalSpace.generateFrom (Set.preimage f '' b)- Defined in
- Mathlib.Topology.Order
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement · cited by 24,529
- Set.imagestatement · cited by 5,609
- Set.preimagestatement and proof · cited by 4,946
- le_antisymmproof · cited by 2,068
- Set.mem_image_of_memproof · cited by 371
- TopologicalSpace.inducedstatement · cited by 148
- Set.forall_mem_imageproof · cited by 65
- TopologicalSpace.generateFromstatement · cited by 62
- le_generateFromproof · cited by 10
- coinduced_le_iff_le_inducedproof · cited by 6
Cited by5
Results whose statement or proof uses this declaration.
- TopologicalSpace.vietoris.isEmbedding_singletonproof · cited by 4
- Topology.IsInducing.image_vietorisproof · cited by 2
- ContinuousMap.isInducing_postcompproof · cited by 2
- TopologicalSpace.secondCountableTopology_inducedproof · cited by 1
- le_induced_generateFromproof · cited by 0