CountableSeparatingOn

📁 Source: Mathlib/Order/Filter/CountableSeparatingOn.lean

Statistics

Metric	Count
Definitions HasCountableSeparatingOn	1
Theorems of_eventually_mem_of_forall_separating_mem_iff, of_eventually_mem_of_forall_separating_preimage, of_forall_separating_mem_iff, of_forall_separating_preimage, exists_eventuallyEq_const_of_eventually_mem_of_forall_separating, exists_eventuallyEq_const_of_forall_separating, exists_mem_eventuallyEq_const_of_eventually_mem_of_forall_separating, exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating, exists_singleton_mem_of_forall_separating, exists_singleton_mem_of_mem_of_forall_separating, exists_subset_subsingleton_mem_of_forall_separating, exists_subsingleton_mem_of_forall_separating, exists_countable_separating, mono, of_subtype, subtype_iff, exists_countable_separating, exists_nonempty_countable_separating, exists_seq_separating	19
Total	20

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eventuallyEq_const_of_eventually_mem_of_forall_separating 📖	mathematical	Eventually Set Set.instMembership	EventuallyEq	—	exists_singleton_mem_of_mem_of_forall_separating instCountableInterFilterMap
exists_eventuallyEq_const_of_forall_separating 📖	mathematical	Eventually Set Set.instMembership	EventuallyEq	—	exists_singleton_mem_of_forall_separating instCountableInterFilterMap
exists_mem_eventuallyEq_const_of_eventually_mem_of_forall_separating 📖	mathematical	Eventually Set Set.instMembership Set.Nonempty	EventuallyEq	—	exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating instCountableInterFilterMap
exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating 📖	mathematical	Set Filter instMembership Set.Nonempty Compl.compl Set.instCompl	Set.instMembership Set.instSingletonSet	—	exists_subset_subsingleton_mem_of_forall_separating Set.Subsingleton.eq_empty_or_singleton mem_of_superset Set.empty_subset
exists_singleton_mem_of_forall_separating 📖	mathematical	Set Filter instMembership Compl.compl Set.instCompl	Set.instSingletonSet	—	exists_singleton_mem_of_mem_of_forall_separating univ_mem
exists_singleton_mem_of_mem_of_forall_separating 📖	mathematical	Set Filter instMembership Compl.compl Set.instCompl	Set.instSingletonSet	—	Set.eq_empty_or_nonempty mem_of_superset Set.empty_subset exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating
exists_subset_subsingleton_mem_of_forall_separating 📖	mathematical	Set Filter instMembership Compl.compl Set.instCompl	Set.instHasSubset Set.Subsingleton	—	HasCountableSeparatingOn.exists_countable_separating inter_mem countable_sInter_mem Set.Countable.mono Set.inter_subset_left countable_bInter_mem iInter_mem'
exists_subsingleton_mem_of_forall_separating 📖	mathematical	Set Filter instMembership Compl.compl Set.instCompl	Set.Subsingleton	—	exists_subset_subsingleton_mem_of_forall_separating univ_mem

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_eventually_mem_of_forall_separating_mem_iff 📖	mathematical	Filter.Eventually Set Set.instMembership	Filter.EventuallyEq	—	HasCountableSeparatingOn.exists_countable_separating eventually_countable_ball Filter.mp_mem Filter.univ_mem'
of_eventually_mem_of_forall_separating_preimage 📖	—	Filter.Eventually Set Set.instMembership Filter.EventuallyEq Set.preimage	—	—	of_eventually_mem_of_forall_separating_mem_iff mem_iff
of_forall_separating_mem_iff 📖	mathematical	Filter.Eventually Set Set.instMembership	Filter.EventuallyEq	—	of_eventually_mem_of_forall_separating_mem_iff Filter.univ_mem
of_forall_separating_preimage 📖	—	Filter.EventuallyEq Set.preimage	—	—	of_eventually_mem_of_forall_separating_preimage Filter.univ_mem

HasCountableSeparatingOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_countable_separating 📖	mathematical	—	Set.Countable Set	—	—
mono 📖	mathematical	Set Set.instHasSubset	HasCountableSeparatingOn	—	exists_countable_separating
of_subtype 📖	mathematical	Set.preimage Set.Elem Set Set.instMembership	HasCountableSeparatingOn	—	exists_countable_separating Set.Countable.image Set.forall_mem_image Set.mem_image_of_mem Function.sometimes_spec
subtype_iff 📖	mathematical	—	HasCountableSeparatingOn Set.Elem Set Set.preimage Set.instMembership Set.univ	—	of_subtype Set.Countable.image Subtype.val_injective Subtype.coe_prop

(root)

Definitions

Name	Category	Theorems
HasCountableSeparatingOn 📖	CompData	14 math math: instHasCountableSeparatingOnIsClosedOfIsOpen, MeasurableSpace.countablySeparated_def, instHasCountableSeparatingOnIsOpenOfT0SpaceOfSecondCountableTopologyElem, HasCountableSeparatingOn.mono, HasCountableSeparatingOn.of_subtype, HasCountableSeparatingOn.range_Ioi, HasCountableSeparatingOn.range_Iio, MeasurableSpace.CountablySeparated.subtype_iff, MeasurableSpace.CountablySeparated.countably_separated, HasCountableSeparatingOn.subtype_iff, MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated, HasCountableSeparatingOn.range_Ici, MeasurableSpace.hasCountableSeparatingOn_of_countablySeparated_subtype, HasCountableSeparatingOn.range_Iic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_countable_separating 📖	mathematical	—	Set.Countable Set	—	HasCountableSeparatingOn.exists_countable_separating
exists_nonempty_countable_separating 📖	mathematical	—	Set.Nonempty Set Set.Countable	—	exists_countable_separating Set.insert_nonempty Set.Countable.insert Set.forall_insert_of_forall Set.forall_of_forall_insert
exists_seq_separating 📖	—	—	—	—	exists_nonempty_countable_separating Set.Countable.exists_eq_range

---

← Back to Index