Hemicontinuity

📁 Source: Mathlib/Topology/Semicontinuity/Hemicontinuity.lean

Statistics

Metric	Count
Definitions	0
Theorems forall_isOpen, inter, isClosed_domain, isInducing_comp, of_forall_isOpen, union, forall_isOpen, inter, isInducing_comp, mem_of_tendsto, of_forall_isOpen, of_sequences, union, forall_isOpen, inter, isInducing_comp, of_forall_isOpen, union, forall_isOpen, inter, isInducing_comp, of_forall_isOpen, union, isClosedMap_iff_upperHemicontinuous, isOpenMap_iff_lowerHemicontinuous, lowerHemicontinuous_iff_isClosed_preimage_Iic, lowerHemicontinuous_iff_isOpen_compl_preimage_Iic_compl, upperHemicontinuousAt_iff_forall_isOpen, upperHemicontinuousAt_iff_preimage_Iic, upperHemicontinuousAt_singleton_iff, upperHemicontinuousOn_iff_forall_isOpen, upperHemicontinuousOn_iff_preimage_Iic, upperHemicontinuousOn_singleton_iff, upperHemicontinuousWithinAt_iff_forall_isOpen, upperHemicontinuousWithinAt_iff_preimage_Iic, upperHemicontinuousWithinAt_singleton_iff, upperHemicontinuous_iff_forall_isOpen, upperHemicontinuous_iff_isClosed_compl_preimage_Iic_compl, upperHemicontinuous_iff_isOpen_preimage_Iic, upperHemicontinuous_iff_preimage_Iic, upperHemicontinuous_singleton_id, upperHemicontinuous_singleton_iff	42
Total	42

UpperHemicontinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall_isOpen 📖	mathematical	UpperHemicontinuous IsOpen Set Set.instHasSubset	Filter.Eventually nhds	—	upperHemicontinuous_iff_forall_isOpen
inter 📖	mathematical	UpperHemicontinuous	Set Set.instInter	—	upperHemicontinuous_iff UpperHemicontinuousAt.inter
isClosed_domain 📖	mathematical	UpperHemicontinuous	IsClosed setOf Set.Nonempty	—	nhdsSet_empty
isInducing_comp 📖	mathematical	UpperHemicontinuous Topology.IsInducing	Set.preimage	—	upperHemicontinuous_iff UpperHemicontinuousAt.isInducing_comp
of_forall_isOpen 📖	mathematical	Filter.Eventually Set Set.instHasSubset nhds	UpperHemicontinuous	—	upperHemicontinuous_iff_forall_isOpen
union 📖	mathematical	UpperHemicontinuous	Set Set.instUnion	—	upperHemicontinuous_iff UpperHemicontinuousAt.union

UpperHemicontinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall_isOpen 📖	mathematical	UpperHemicontinuousAt IsOpen Set Set.instHasSubset	Filter.Eventually nhds	—	upperHemicontinuousAt_iff_forall_isOpen
inter 📖	mathematical	UpperHemicontinuousAt	Set Set.instInter	—	upperHemicontinuousWithinAt_univ_iff UpperHemicontinuousWithinAt.inter
isInducing_comp 📖	mathematical	UpperHemicontinuousAt Topology.IsInducing	Set.preimage	—	UpperHemicontinuousWithinAt.isInducing_comp upperHemicontinuousWithinAt
mem_of_tendsto 📖	—	UpperHemicontinuousAt Filter.Tendsto nhds Filter.Frequently Set Set.instMembership	—	—	Filter.disjoint_iff RegularSpace.regular Filter.Frequently.mp Filter.mp_mem Filter.univ_mem' interior_subset Disjoint.notMem_of_mem_left
of_forall_isOpen 📖	mathematical	Filter.Eventually Set Set.instHasSubset nhds	UpperHemicontinuousAt	—	upperHemicontinuousAt_iff_forall_isOpen
of_sequences 📖	mathematical	IsSeqCompact Filter.Eventually Set Set.instHasSubset nhds Set.instMembership	UpperHemicontinuousAt	—	of_frequently Filter.exists_seq_forall_of_frequently IsSeqCompact.subseq_of_frequently_in Filter.Eventually.frequently Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.mp_mem Filter.univ_mem' Filter.Tendsto.comp StrictMono.tendsto_atTop mem_closure_of_tendsto IsClosed.closure_eq Filter.Eventually.of_forall
union 📖	mathematical	UpperHemicontinuousAt	Set Set.instUnion	—	upperHemicontinuousWithinAt_univ_iff UpperHemicontinuousWithinAt.union

UpperHemicontinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall_isOpen 📖	mathematical	UpperHemicontinuousOn Set Set.instMembership IsOpen Set.instHasSubset	Filter.Eventually nhdsWithin	—	upperHemicontinuousOn_iff_forall_isOpen
inter 📖	mathematical	UpperHemicontinuousOn	Set Set.instInter	—	upperHemicontinuousOn_iff UpperHemicontinuousWithinAt.inter
isInducing_comp 📖	mathematical	UpperHemicontinuousOn Topology.IsInducing	Set.preimage	—	upperHemicontinuousOn_iff UpperHemicontinuousWithinAt.isInducing_comp
of_forall_isOpen 📖	mathematical	Filter.Eventually Set Set.instHasSubset nhdsWithin	UpperHemicontinuousOn	—	upperHemicontinuousOn_iff_forall_isOpen
union 📖	mathematical	UpperHemicontinuousOn	Set Set.instUnion	—	upperHemicontinuousOn_iff UpperHemicontinuousWithinAt.union

UpperHemicontinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forall_isOpen 📖	mathematical	UpperHemicontinuousWithinAt IsOpen Set Set.instHasSubset	Filter.Eventually nhdsWithin	—	upperHemicontinuousWithinAt_iff_forall_isOpen
inter 📖	mathematical	UpperHemicontinuousWithinAt	Set Set.instInter	—	upperHemicontinuousWithinAt_iff_forall_isOpen IsOpen.union IsClosed.isOpen_compl
isInducing_comp 📖	mathematical	UpperHemicontinuousWithinAt Topology.IsInducing	Set.preimage	—	of_forall_isOpen Topology.IsInducing.isOpen_iff Set.preimage_inter_range Set.preimage_subset_preimage_iff Set.inter_subset_right forall_isOpen inter
of_forall_isOpen 📖	mathematical	Filter.Eventually Set Set.instHasSubset nhdsWithin	UpperHemicontinuousWithinAt	—	upperHemicontinuousWithinAt_iff_forall_isOpen
union 📖	mathematical	UpperHemicontinuousWithinAt	Set Set.instUnion	—	upperHemicontinuousWithinAt_iff nhdsSet_union

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosedMap_iff_upperHemicontinuous 📖	mathematical	—	IsClosedMap UpperHemicontinuous Set.preimage Set Set.instSingletonSet	—	isClosedMap_iff_kernImage upperHemicontinuous_iff_isOpen_preimage_Iic
isOpenMap_iff_lowerHemicontinuous 📖	mathematical	—	IsOpenMap LowerHemicontinuous Set.preimage Set Set.instSingletonSet	—	isOpenMap_iff_kernImage lowerHemicontinuous_iff_isClosed_preimage_Iic
lowerHemicontinuous_iff_isClosed_preimage_Iic 📖	mathematical	—	LowerHemicontinuous IsClosed Set.preimage Set Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	Function.Surjective.forall compl_surjective compl_compl lowerHemicontinuous_iff_isOpen_compl_preimage_Iic_compl
lowerHemicontinuous_iff_isOpen_compl_preimage_Iic_compl 📖	mathematical	—	LowerHemicontinuous IsOpen Compl.compl Set Set.instCompl Set.preimage Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	forall_swap
upperHemicontinuousAt_iff_forall_isOpen 📖	mathematical	—	UpperHemicontinuousAt Filter.Eventually Set Set.instHasSubset nhds	—	nhdsWithin_univ upperHemicontinuousWithinAt_iff_forall_isOpen
upperHemicontinuousAt_iff_preimage_Iic 📖	mathematical	—	UpperHemicontinuousAt Set Filter Filter.instMembership nhds Set.preimage Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	nhdsWithin_univ upperHemicontinuousWithinAt_iff_preimage_Iic
upperHemicontinuousAt_singleton_iff 📖	mathematical	—	UpperHemicontinuousAt Set Set.instSingletonSet ContinuousAt	—	—
upperHemicontinuousOn_iff_forall_isOpen 📖	mathematical	—	UpperHemicontinuousOn Filter.Eventually Set Set.instHasSubset nhdsWithin	—	—
upperHemicontinuousOn_iff_preimage_Iic 📖	mathematical	—	UpperHemicontinuousOn Set Filter Filter.instMembership nhdsWithin Set.preimage Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	—
upperHemicontinuousOn_singleton_iff 📖	mathematical	—	UpperHemicontinuousOn Set Set.instSingletonSet ContinuousOn	—	upperHemicontinuousWithinAt_singleton_iff
upperHemicontinuousWithinAt_iff_forall_isOpen 📖	mathematical	—	UpperHemicontinuousWithinAt Filter.Eventually Set Set.instHasSubset nhdsWithin	—	upperHemicontinuousWithinAt_iff Filter.HasBasis.forall_iff hasBasis_nhdsSet Filter.Eventually.mp Filter.Eventually.of_forall Filter.mem_of_superset IsOpen.interior_eq
upperHemicontinuousWithinAt_iff_preimage_Iic 📖	mathematical	—	UpperHemicontinuousWithinAt Set Filter Filter.instMembership nhdsWithin Set.preimage Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	Filter.HasBasis.forall_iff hasBasis_nhdsSet Filter.mp_mem Filter.univ_mem' Filter.mem_of_superset Set.preimage_mono IsOpen.mem_nhdsSet
upperHemicontinuousWithinAt_singleton_iff 📖	mathematical	—	UpperHemicontinuousWithinAt Set Set.instSingletonSet ContinuousWithinAt	—	nhdsSet_singleton Filter.mp_mem Filter.univ_mem' mem_of_mem_nhds UpperHemicontinuousWithinAt.comp UpperHemicontinuous.upperHemicontinuousWithinAt upperHemicontinuous_singleton_id Set.mapsTo_image
upperHemicontinuous_iff_forall_isOpen 📖	mathematical	—	UpperHemicontinuous Filter.Eventually Set Set.instHasSubset nhds	—	—
upperHemicontinuous_iff_isClosed_compl_preimage_Iic_compl 📖	mathematical	—	UpperHemicontinuous IsClosed Compl.compl Set Set.instCompl Set.preimage Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	Function.Surjective.forall compl_surjective compl_compl upperHemicontinuous_iff_isOpen_preimage_Iic
upperHemicontinuous_iff_isOpen_preimage_Iic 📖	mathematical	—	UpperHemicontinuous IsOpen Set.preimage Set Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	isOpen_iff_mem_nhds Filter.HasBasis.forall_iff hasBasis_nhdsSet Filter.mem_of_superset Set.preimage_mono forall_swap
upperHemicontinuous_iff_preimage_Iic 📖	mathematical	—	UpperHemicontinuous Set Filter Filter.instMembership nhds Set.preimage Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	—
upperHemicontinuous_singleton_id 📖	mathematical	—	UpperHemicontinuous Set Set.instSingletonSet	—	nhdsSet_singleton
upperHemicontinuous_singleton_iff 📖	mathematical	—	UpperHemicontinuous Set Set.instSingletonSet Continuous	—	—

---

← Back to Index