Commit 2023-06-14 00:07 9c20de92

View on Github →

feat: port Topology.ContinuousFunction.Ideals (#4852)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Algebra/Ring/Ideal.lean

modified theorem Ideal.closure_eq_of_isClosed

Created Mathlib/Topology/ContinuousFunction/Ideals.lean

added theorem ContinuousMap.exists_mul_le_one_eqOn_ge

added theorem ContinuousMap.idealOfEmpty_eq_bot

added def ContinuousMap.idealOfSet

added theorem ContinuousMap.idealOfSet_closed

added theorem ContinuousMap.idealOfSet_isMaximal_iff

added theorem ContinuousMap.idealOfSet_ofIdeal_eq_closure

added theorem ContinuousMap.idealOfSet_ofIdeal_isClosed

added theorem ContinuousMap.idealOf_compl_singleton_isMaximal

added def ContinuousMap.idealOpensGI

added theorem ContinuousMap.ideal_gc

added theorem ContinuousMap.ideal_isMaximal_iff

added theorem ContinuousMap.mem_idealOfSet

added theorem ContinuousMap.mem_idealOfSet_compl_singleton

added theorem ContinuousMap.mem_setOfIdeal

added theorem ContinuousMap.not_mem_idealOfSet

added theorem ContinuousMap.not_mem_setOfIdeal

added def ContinuousMap.opensOfIdeal

added def ContinuousMap.setOfIdeal

added theorem ContinuousMap.setOfIdeal_eq_compl_singleton

added theorem ContinuousMap.setOfIdeal_ofSet_eq_interior

added theorem ContinuousMap.setOfIdeal_ofSet_of_isOpen

added theorem ContinuousMap.setOfIdeal_open

added theorem ContinuousMap.setOfTop_eq_univ

added def WeakDual.CharacterSpace.continuousMapEval

added theorem WeakDual.CharacterSpace.continuousMapEval_apply_apply

added theorem WeakDual.CharacterSpace.continuousMapEval_bijective