Commit 2023-01-31 11:16 7be5fc92

View on Github →

feat: port Topology.Order (#1843)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Basic.lean

Created Mathlib/Topology/Order.lean

added theorem Continuous.coinduced_le

added theorem Continuous.le_induced

added theorem Equiv.coinduced_symm

added theorem Equiv.induced_symm

added theorem IsClosed.mono

added theorem IsOpen.mono

added inductive TopologicalSpace.GenerateOpen

added def TopologicalSpace.coinduced

added theorem TopologicalSpace.gc_generateFrom

added def TopologicalSpace.gciGenerateFrom

added def TopologicalSpace.generateFrom

added theorem TopologicalSpace.generateFrom_anti

added theorem TopologicalSpace.generateFrom_setOf_isOpen

added theorem TopologicalSpace.generateFrom_surjective

added def TopologicalSpace.induced

added theorem TopologicalSpace.isOpen_generateFrom_of_mem

added theorem TopologicalSpace.isOpen_top_iff

added theorem TopologicalSpace.le_generateFrom_iff_subset_isOpen

added theorem TopologicalSpace.leftInverse_generateFrom

added theorem TopologicalSpace.mkOfClosure_sets

added theorem TopologicalSpace.nhds_generateFrom

added theorem TopologicalSpace.nhds_mkOfNhds

added theorem TopologicalSpace.nhds_mkOfNhds_filterBasis

added theorem TopologicalSpace.nhds_mkOfNhds_single

added theorem TopologicalSpace.setOf_isOpen_injective

added theorem TopologicalSpace.tendsto_nhds_generateFrom

added theorem closure_induced

added theorem coinduced_bot

added theorem coinduced_compose

added theorem coinduced_id

added theorem coinduced_le_iff_le_induced

added theorem coinduced_mono

added theorem coinduced_sup

added theorem coinduced_supᵢ

added theorem continuous_Prop

added theorem continuous_bot

added theorem continuous_coinduced_dom

added theorem continuous_coinduced_rng

added theorem continuous_empty_function

added theorem continuous_generateFrom

added theorem continuous_id_iff_le

added theorem continuous_id_of_le

added theorem continuous_iff_coinduced_le

added theorem continuous_iff_le_induced

added theorem continuous_induced_dom

added theorem continuous_induced_rng

added theorem continuous_inf_dom_left

added theorem continuous_inf_dom_right

added theorem continuous_inf_rng

added theorem continuous_infᵢ_dom

added theorem continuous_infᵢ_rng

added theorem continuous_infₛ_dom

added theorem continuous_infₛ_rng

added theorem continuous_le_dom

added theorem continuous_le_rng

added theorem continuous_of_discreteTopology

added theorem continuous_sup_dom

added theorem continuous_sup_rng_left

added theorem continuous_sup_rng_right

added theorem continuous_supᵢ_dom

added theorem continuous_supᵢ_rng

added theorem continuous_supₛ_dom

added theorem continuous_supₛ_rng

added theorem continuous_top

added theorem discreteTopology_bot

added theorem discreteTopology_iff_nhds

added theorem discreteTopology_iff_nhds_ne

added theorem discreteTopology_iff_singleton_mem_nhds

added theorem eq_bot_of_singletons_open

added theorem eq_of_nhds_eq_nhds

added theorem forall_open_iff_discrete

added theorem gc_coinduced_induced

added theorem gc_nhds

added theorem generateFrom_inter

added theorem generateFrom_interᵢ

added theorem generateFrom_interᵢ_of_generateFrom_eq_self

added theorem generateFrom_union

added theorem generateFrom_union_isOpen

added theorem generateFrom_unionᵢ

added theorem generateFrom_unionᵢ_isOpen

added theorem generateFrom_unionₛ

added theorem induced_compose

added theorem induced_const

added theorem induced_generateFrom_eq

added theorem induced_id

added theorem induced_iff_nhds_eq

added theorem induced_inf

added theorem induced_infᵢ

added theorem induced_mono

added theorem induced_top

added theorem isClosed_discrete

added theorem isClosed_induced_iff'

added theorem isClosed_induced_iff

added theorem isClosed_supᵢ_iff

added theorem isOpen_coinduced

added theorem isOpen_discrete

added theorem isOpen_iff_continuous_mem

added theorem isOpen_implies_isOpen_iff

added theorem isOpen_induced

added theorem isOpen_induced_eq

added theorem isOpen_induced_iff

added theorem isOpen_singleton_nhdsAdjoint

added theorem isOpen_singleton_true

added theorem isOpen_sup

added theorem isOpen_supᵢ_iff

added theorem le_generateFrom

added theorem le_iff_nhds

added theorem le_induced_generateFrom

added theorem le_nhdsAdjoint_iff'

added theorem le_nhdsAdjoint_iff

added theorem le_of_nhds_le_nhds

added theorem map_nhds_induced_eq

added theorem map_nhds_induced_of_mem

added theorem map_nhds_induced_of_surjective

added theorem mem_nhds_discrete

added theorem mem_nhds_induced

added def nhdsAdjoint

added theorem nhdsAdjoint_nhds

added theorem nhdsAdjoint_nhds_of_ne

added theorem nhds_discrete

added theorem nhds_false

added theorem nhds_induced

added theorem nhds_inf

added theorem nhds_infᵢ

added theorem nhds_infₛ

added theorem nhds_mono

added theorem nhds_top

added theorem nhds_true

added theorem preimage_nhds_coinduced

added theorem setOf_isOpen_sup

added theorem setOf_isOpen_supᵢ

added theorem setOf_isOpen_supₛ

added theorem singletons_open_iff_discrete