Ideals

📁 Source: Mathlib/Topology/ContinuousMap/Ideals.lean

Statistics

Metric	Count
Definitions idealOfSet, idealOpensGI, opensOfIdeal, setOfIdeal, continuousMapEval, homeoEval	6
Theorems coe_opensOfIdeal, exists_mul_le_one_eqOn_ge, idealOfEmpty_eq_bot, idealOfSet_closed, idealOfSet_isMaximal_iff, idealOfSet_ofIdeal_eq_closure, idealOfSet_ofIdeal_isClosed, idealOf_compl_singleton_isMaximal, idealOpensGI_choice, ideal_gc, ideal_isMaximal_iff, mem_idealOfSet, mem_idealOfSet_compl_singleton, mem_setOfIdeal, notMem_idealOfSet, notMem_setOfIdeal, setOfIdeal_eq_compl_singleton, setOfIdeal_ofSet_eq_interior, setOfIdeal_ofSet_of_isOpen, setOfIdeal_open, setOfTop_eq_univ, continuousMapEval_apply_apply, continuousMapEval_bijective	23
Total	29

ContinuousMap

Definitions

Name	Category	Theorems
idealOfSet 📖	CompOp	14 math math: setOfIdeal_ofSet_eq_interior, notMem_idealOfSet, mem_idealOfSet, setOfIdeal_ofSet_of_isOpen, idealOfSet_closed, ideal_isMaximal_iff, ideal_gc, idealOfEmpty_eq_bot, mem_idealOfSet_compl_singleton, idealOf_compl_singleton_isMaximal, idealOfSet_ofIdeal_isClosed, idealOfSet_ofIdeal_eq_closure, idealOfSet_isMaximal_iff, idealOpensGI_choice
idealOpensGI 📖	CompOp	1 math math: idealOpensGI_choice
opensOfIdeal 📖	CompOp	2 math math: coe_opensOfIdeal, idealOpensGI_choice
setOfIdeal 📖	CompOp	11 math math: setOfIdeal_ofSet_eq_interior, setOfIdeal_ofSet_of_isOpen, notMem_setOfIdeal, setOfIdeal_eq_compl_singleton, ideal_gc, setOfTop_eq_univ, coe_opensOfIdeal, mem_setOfIdeal, setOfIdeal_open, idealOfSet_ofIdeal_isClosed, idealOfSet_ofIdeal_eq_closure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_opensOfIdeal 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike opensOfIdeal setOfIdeal	—	—
exists_mul_le_one_eqOn_ge 📖	mathematical	NNReal Preorder.toLT PartialOrder.toPreorder NNReal.instPartialOrder NNReal.instZero	ContinuousMap NNReal NNReal.instTopologicalSpace Preorder.toLE PartialOrder.toPreorder NNReal.instPartialOrder DFunLike.coe instFunLike instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring IsTopologicalSemiring.toContinuousMul NNReal.instIsTopologicalSemiring NNReal.instOne Set.EqOn Pi.instOne setOf	—	IsTopologicalSemiring.toContinuousMul NNReal.instIsTopologicalSemiring Continuous.inv₀ NNReal.instContinuousInv₀ Continuous.sup TopologicalLattice.toContinuousSup LinearOrder.topologicalLattice OrderTopology.to_orderClosedTopology NNReal.instOrderTopology ContinuousMapClass.map_continuous instContinuousMapClass LT.lt.ne' LT.lt.trans_le le_sup_right inv_mul_le_iff₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono le_sup_left mul_one sup_eq_left Set.mem_setOf inv_mul_cancel₀
idealOfEmpty_eq_bot 📖	mathematical	—	idealOfSet Set Set.instEmptyCollection Bot.bot Ideal ContinuousMap instSemiringOfIsTopologicalSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.ext Set.compl_empty
idealOfSet_closed 📖	mathematical	—	IsClosed ContinuousMap compactOpen SetLike.coe Ideal instSemiringOfIsTopologicalSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule idealOfSet	—	Set.setOf_forall isClosed_iInter isClosed_eq ContinuousEvalConst.continuous_eval_const instContinuousEvalConst continuous_const
idealOfSet_isMaximal_iff 📖	mathematical	—	Ideal.IsMaximal ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instSemiringOfIsTopologicalSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing idealOfSet SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike IsCoatom PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder BoundedOrder.toOrderTop Preorder.toLE CompleteLattice.toBoundedOrder TopologicalSpace.Opens.instCompleteLattice	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Ideal.isMaximal_def GaloisInsertion.isCoatom_iff Ideal.instIsCoatomic TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace idealOfSet_ofIdeal_isClosed Ideal.IsMaximal.isClosed instHasSummableGeomSeriesOfCompleteSpace instCompleteSpaceOfCompactlyCoherentSpace RCLike.toCompleteSpace CompactlyCoherentSpace.of_weaklyLocallyCompactSpace instWeaklyLocallyCompactSpaceOfCompactSpace
idealOfSet_ofIdeal_eq_closure 📖	mathematical	—	idealOfSet DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing setOfIdeal Ideal.closure ContinuousMap compactOpen instRing NormedRing.toRing NormedCommRing.toNormedRing instIsTopologicalRingOfLocallyCompactSpace WeaklyLocallyCompactSpace.locallyCompactSpace T2Space.r1Space instWeaklyLocallyCompactSpaceOfCompactSpace NonUnitalNormedRing.toNonUnitalRing NonUnitalNormedCommRing.toNonUnitalNormedRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing le_antisymm instIsTopologicalRingOfLocallyCompactSpace WeaklyLocallyCompactSpace.locallyCompactSpace T2Space.r1Space instWeaklyLocallyCompactSpaceOfCompactSpace Metric.mem_closure_iff CanLift.prf NNReal.canLift LT.lt.le GT.gt.lt Nat.instAtLeastTwoHAddOfNat isClosed_le OrderTopology.to_orderClosedTopology NNReal.instOrderTopology continuous_const Continuous.nnnorm ContinuousMapClass.map_continuous instContinuousMapClass Set.subset_compl_iff_disjoint_left Eq.trans_lt nnnorm_eq_zero mem_idealOfSet half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass NNReal.instContinuousSMulOfReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsCompact.induction_on IsClosed.isCompact ext map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass Ideal.zero_mem IsSemitopologicalSemiring.toContinuousAdd IsTopologicalSemiring.toIsSemitopologicalSemiring NNReal.instIsTopologicalSemiring map_add SemilinearMapClass.toAddHomClass IsStrictOrderedRing.toCharZero RCLike.charZero_rclike RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass Ideal.add_mem zero_add add_lt_add_of_lt_of_le NNReal.addLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid NNReal.addLeftReflectLT covariant_swap_add_of_covariant_add zero_le' add_lt_add_of_le_of_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono Disjoint.subset_compl_right mem_setOfIdeal compl_compl ContinuousAt.eventually_ne T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Continuous.continuousAt mem_nhdsWithin_iff_exists_mem_nhds_inter Set.Subset.rfl Continuous.pow IsTopologicalSemiring.toContinuousMul RCLike.instContinuousStar map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RCLike.conj_mul Ideal.mul_mem_left pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass norm_pos_iff Set.eq_empty_or_nonempty zero_lt_one LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.charZero_one IsCompact.exists_isMinOn instClosedIicTopology Continuous.continuousOn exists_mul_le_one_eqOn_ge map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Set.EqOn.mono nndist_eq_nnnorm nnnorm_lt_iff map_one MonoidHomClass.toOneHomClass mul_one sub_self nnnorm_zero lt_of_le_of_lt IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Algebra.algebraMap_eq_smul_one NNReal.coe_sub sub_smul one_smul Eq.trans_le nnnorm_algebraMap_nnreal NormedDivisionRing.to_normOneClass tsub_le_self mul_sub LE.le.trans nnnorm_mul_le mul_le_mul_left covariant_swap_mul_of_covariant_mul NNReal.mulLeftMono not_le mul_le_mul_right half_lt_self IsClosed.closure_subset_iff idealOfSet_closed notMem_setOfIdeal
idealOfSet_ofIdeal_isClosed 📖	mathematical	—	idealOfSet DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing setOfIdeal	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing instIsTopologicalRingOfLocallyCompactSpace WeaklyLocallyCompactSpace.locallyCompactSpace T2Space.r1Space instWeaklyLocallyCompactSpaceOfCompactSpace idealOfSet_ofIdeal_eq_closure Ideal.ext Set.ext_iff IsClosed.closure_eq
idealOf_compl_singleton_isMaximal 📖	mathematical	—	Ideal.IsMaximal ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instSemiringOfIsTopologicalSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing idealOfSet Compl.compl Set Set.instCompl Set.instSingletonSet	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing T2Space.t1Space idealOfSet_isMaximal_iff TopologicalSpace.Opens.isCoatom_iff
idealOpensGI_choice 📖	mathematical	Ideal ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instSemiringOfIsTopologicalSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule idealOfSet SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike opensOfIdeal	GaloisInsertion.choice Ideal ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instSemiringOfIsTopologicalSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing TopologicalSpace.Opens PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule TopologicalSpace.Opens.instPartialOrder opensOfIdeal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedField.toMetricSpace idealOfSet SetLike.coe TopologicalSpace.Opens.instSetLike idealOpensGI Ideal.closure compactOpen instRing NormedRing.toRing NormedCommRing.toNormedRing	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
ideal_gc 📖	mathematical	—	GaloisConnection Ideal ContinuousMap instSemiringOfIsTopologicalSemiring Set PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra setOfIdeal idealOfSet	—	notMem_idealOfSet notMem_setOfIdeal mem_setOfIdeal
ideal_isMaximal_iff 📖	mathematical	—	Ideal.IsMaximal ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instSemiringOfIsTopologicalSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing idealOfSet Compl.compl Set Set.instCompl Set.instSingletonSet	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing setOfIdeal_eq_compl_singleton instIsTopologicalRingOfLocallyCompactSpace WeaklyLocallyCompactSpace.locallyCompactSpace T2Space.r1Space instWeaklyLocallyCompactSpaceOfCompactSpace idealOfSet_ofIdeal_eq_closure Ideal.closure_eq_of_isClosed idealOf_compl_singleton_isMaximal
mem_idealOfSet 📖	mathematical	—	ContinuousMap Ideal instSemiringOfIsTopologicalSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule idealOfSet DFunLike.coe instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
mem_idealOfSet_compl_singleton 📖	mathematical	—	ContinuousMap Ideal instSemiringOfIsTopologicalSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule idealOfSet Compl.compl Set Set.instCompl Set.instSingletonSet DFunLike.coe instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	compl_compl
mem_setOfIdeal 📖	mathematical	—	Set Set.instMembership setOfIdeal ContinuousMap Ideal instSemiringOfIsTopologicalSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Mathlib.Tactic.Push.not_forall_eq
notMem_idealOfSet 📖	mathematical	—	ContinuousMap Ideal instSemiringOfIsTopologicalSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule idealOfSet Set Set.instMembership Compl.compl Set.instCompl	—	Mathlib.Tactic.Push.not_forall_eq
notMem_setOfIdeal 📖	mathematical	—	Set Set.instMembership setOfIdeal DFunLike.coe ContinuousMap instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	Set.mem_compl_iff setOfIdeal.eq_1 compl_compl Set.mem_setOf
setOfIdeal_eq_compl_singleton 📖	mathematical	—	setOfIdeal DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Compl.compl Set Set.instCompl Set.instSingletonSet	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing idealOfSet_ofIdeal_isClosed Ideal.IsMaximal.isClosed instHasSummableGeomSeriesOfCompleteSpace instCompleteSpaceOfCompactlyCoherentSpace RCLike.toCompleteSpace CompactlyCoherentSpace.of_weaklyLocallyCompactSpace instWeaklyLocallyCompactSpaceOfCompactSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace T2Space.t1Space TopologicalSpace.Opens.isCoatom_iff idealOfSet_isMaximal_iff
setOfIdeal_ofSet_eq_interior 📖	mathematical	—	setOfIdeal DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing idealOfSet interior	—	Set.Subset.antisymm IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsOpen.subset_interior_iff setOfIdeal_open TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace mem_setOfIdeal Set.notMem_compl_iff exists_continuous_zero_one_of_isClosed NormalSpace.of_regularSpace_lindelofSpace instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space instWeaklyLocallyCompactSpaceOfCompactSpace T2Space.r1Space instLindelofSpaceOfSigmaCompactSpace CompactSpace.sigmaCompact isClosed_closure isClosed_singleton T2Space.t1Space Set.disjoint_singleton_right closure_compl compl_compl Continuous.comp RCLike.continuous_ofReal ContinuousMapClass.map_continuous instContinuousMapClass subset_closure Set.mem_singleton RCLike.ofReal_one one_ne_zero NeZero.charZero_one RCLike.charZero_rclike
setOfIdeal_ofSet_of_isOpen 📖	mathematical	IsOpen	setOfIdeal DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing idealOfSet	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing setOfIdeal_ofSet_eq_interior IsOpen.interior_eq
setOfIdeal_open 📖	mathematical	—	IsOpen setOfIdeal	—	Set.setOf_forall isClosed_iInter isClosed_eq ContinuousMapClass.map_continuous instContinuousMapClass continuous_const
setOfTop_eq_univ 📖	mathematical	—	setOfIdeal Top.top Ideal ContinuousMap instSemiringOfIsTopologicalSemiring Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Set.univ	—	Set.univ_subset_iff mem_setOfIdeal Submodule.mem_top one_ne_zero NeZero.one

WeakDual.CharacterSpace

Definitions

Name	Category	Theorems
continuousMapEval 📖	CompOp	2 math math: continuousMapEval_bijective, continuousMapEval_apply_apply
homeoEval 📖	CompOp	1 math math: homeoEval_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousMapEval_apply_apply 📖	mathematical	—	DFunLike.coe Set.Elem WeakDual ContinuousMap CommRing.toCommSemiring IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalNonAssocSemiring.toAddCommMonoid ContinuousMap.instNonUnitalNonAssocSemiringOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring ContinuousMap.module Semiring.toModule ContinuousMap.compactOpen WeakDual.characterSpace instFunLike instTopologicalSpaceSubtype Set Set.instMembership instTopologicalSpaceWeakDual ContinuousMap.instFunLike continuousMapEval	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsTopologicalRing.toIsTopologicalSemiring
continuousMapEval_bijective 📖	mathematical	—	Function.Bijective Set.Elem WeakDual ContinuousMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField CommRing.toCommSemiring Field.toCommRing NormedField.toField IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing SeparatelyContinuousMul.to_continuousSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalNonAssocSemiring.toAddCommMonoid ContinuousMap.instNonUnitalNonAssocSemiringOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring ContinuousMap.module Semiring.toModule ContinuousMap.compactOpen WeakDual.characterSpace DFunLike.coe instTopologicalSpaceSubtype Set Set.instMembership instTopologicalSpaceWeakDual ContinuousMap.instFunLike continuousMapEval IsSimpleRing.instNontrivial NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing DivisionRing.isSimpleRing NormMulClass.toNoZeroDivisors NormedCommRing.toNormedRing NormedDivisionRing.toNormMulClass	—	IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsSimpleRing.instNontrivial DivisionRing.isSimpleRing NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Mathlib.Tactic.Contrapose.contrapose₁ exists_continuous_zero_one_of_isClosed NormalSpace.of_regularSpace_lindelofSpace instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space instWeaklyLocallyCompactSpaceOfCompactSpace T2Space.r1Space instLindelofSpaceOfSigmaCompactSpace CompactSpace.sigmaCompact isClosed_singleton T2Space.t1Space Set.disjoint_singleton DFunLike.ne_iff RCLike.continuous_ofReal zero_ne_one NeZero.charZero_one RCLike.charZero_rclike Set.mem_singleton AlgHomClass.toRingHomClass instAlgHomClass ContinuousMap.ideal_isMaximal_iff Ideal.IsMaximal.isClosed instHasSummableGeomSeriesOfCompleteSpace ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace RCLike.toCompleteSpace CompactlyCoherentSpace.of_weaklyLocallyCompactSpace WeakDual.ker_isMaximal ext_ker Ideal.ext SetLike.ext_iff

---

← Back to Index