IndicatorConstPointwise

📁 Source: Mathlib/Topology/IndicatorConstPointwise.lean

Statistics

Metric	Count
Definitions	0
Theorems tendsto_indicator_const_apply_iff_eventually, tendsto_indicator_const_apply_iff_eventually', tendsto_indicator_const_iff_forall_eventually, tendsto_indicator_const_iff_forall_eventually', tendsto_indicator_const_iff_tendsto_pi_pure, tendsto_indicator_const_iff_tendsto_pi_pure', tendsto_ite	7
Total	7

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_indicator_const_apply_iff_eventually 📖	mathematical	—	Filter.Tendsto Set.indicator nhds Filter.Eventually Set Set.instMembership	—	tendsto_indicator_const_apply_iff_eventually'
tendsto_indicator_const_apply_iff_eventually' 📖	mathematical	Set Filter Filter.instMembership nhds Compl.compl Set.instCompl Set.instSingletonSet	Filter.Tendsto Set.indicator Filter.Eventually Set.instMembership	—	tendsto_ite Filter.principal_singleton mem_of_mem_nhds Set.indicator_of_mem Set.indicator_of_notMem
tendsto_indicator_const_iff_forall_eventually 📖	mathematical	—	Filter.Tendsto Set.indicator nhds Pi.topologicalSpace Filter.Eventually Set Set.instMembership	—	tendsto_indicator_const_iff_forall_eventually'
tendsto_indicator_const_iff_forall_eventually' 📖	mathematical	Set Filter Filter.instMembership nhds Compl.compl Set.instCompl Set.instSingletonSet	Filter.Tendsto Set.indicator Pi.topologicalSpace Filter.Eventually Set.instMembership	—	tendsto_indicator_const_apply_iff_eventually'
tendsto_indicator_const_iff_tendsto_pi_pure 📖	mathematical	—	Filter.Tendsto Set.indicator nhds Pi.topologicalSpace Set Filter.pi Filter Filter.instPure Set.instMembership	—	tendsto_indicator_const_iff_forall_eventually Filter.tendsto_pi
tendsto_indicator_const_iff_tendsto_pi_pure' 📖	mathematical	Set Filter Filter.instMembership nhds Compl.compl Set.instCompl Set.instSingletonSet	Filter.Tendsto Set.indicator Pi.topologicalSpace Filter.pi Filter.instPure Set.instMembership	—	tendsto_indicator_const_iff_forall_eventually' Filter.tendsto_pi
tendsto_ite 📖	mathematical	Set Filter Filter.instMembership Compl.compl Set.instCompl Set.instSingletonSet Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.principal	Filter.Tendsto Filter.Eventually	—	Filter.mp_mem Filter.mem_map Filter.univ_mem' Filter.Tendsto.congr' le_trans Filter.principal_singleton Set.preimage_const_of_mem

---

← Back to Index