FLT/Mathlib/Topology/Algebra/Group/Basic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Lemmas about topological groups

Imports (1)
Imported by 3 files
  1. lemma continuous_iff_continuousAt_one line 15 source

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

    Statement uses: TopologicalSpace, Group, IsTopologicalGroup, MulOneClass, ContinuousMul, FunLike, MonoidHomClass, Iff, Continuous, ContinuousAt, OfNat.ofNat

    Proof uses: Iff.intro, Continuous.continuousAt, continuous_of_continuousAt_one

    22 instances, coercions and auxiliary constants left out.

  2. lemma MonoidHom.continuous_of_isOpen_ker line 23 source

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

    Statement uses: Group, MulOneClass, MonoidHom, TopologicalSpace, IsTopologicalGroup, ContinuousMul, IsOpen, Subgroup, MonoidHom.ker, Continuous

    Proof uses: continuous_of_continuousAt_one, Set, Membership.mem, Filter, nhds, OfNat.ofNat, Eq.mpr, Filter.map, Set.preimage, id, Eq, Filter.mem_of_superset, IsOpen.mem_nhds, of_eq_true, Eq.trans, True, Set.preimage_mono, Singleton.singleton, Iff.mpr, LE.le and 6 more

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  3. lemma MonoidHom.continuous_iff_isOpen_ker line 33 source

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

    Statement uses: Group, MulOneClass, MonoidHom, TopologicalSpace, IsTopologicalGroup, DiscreteTopology, Iff, Continuous, IsOpen, Subgroup, MonoidHom.ker

    Proof uses: Iff.intro, IsOpen.preimage, Singleton.singleton, Set, OfNat.ofNat, isOpen_discrete, MonoidHom.continuous_of_isOpen_ker

    21 instances, coercions and auxiliary constants left out.