FLT/Mathlib/Topology/Polish.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma open_of_locally_compact_dense_metrizable line 25 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: TopologicalSpace, T2Space, LocallyCompactSpace, Continuous, Topology.IsInducing, DenseRange, IsOpen, Set.range

   Proof uses: Eq.mpr, Membership.mem, Set, Filter, nhds, id, Eq, congrArg, propext, isOpen_iff_mem_nhds, Exists, And, LE.le, mem_nhds_iff, Eq.mp, Set.mem_range, IsCompact, closure, exists_isOpen_mem_isCompact_closure, Set.preimage and 22 more

   19 instances, coercions and auxiliary constants left out.

   Tactic trace: 36 steps

   Open to load the checked before-and-after goal states.

2. theorem polish_of_locally_compact_second_countable line 65 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: TopologicalSpace, SecondCountableTopology, T2Space, LocallyCompactSpace, PolishSpace

   Proof uses: TopologicalSpace.MetrizableSpace, MetricSpace, TopologicalSpace.metrizableSpaceMetric, IsOpen, UniformSpace.Completion, Set.range, open_of_locally_compact_dense_metrizable, UniformSpace.Completion.continuous_coe, IsDenseInducing.isInducing, UniformSpace.Completion.isDenseInducing_coe, UniformSpace.Completion.denseRange_coe, Membership.mem, Set, IsOpen.polishSpace, Homeomorph, Topology.IsEmbedding.toHomeomorph, Isometry.isEmbedding, UniformSpace.Completion.coe_isometry, Topology.IsClosedEmbedding.polishSpace, Homeomorph.isClosedEmbedding

   33 instances, coercions and auxiliary constants left out.

   Tactic trace: 13 steps

   Open to load the checked before-and-after goal states.