EventuallyMeasurable

📁 Source: Mathlib/MeasureTheory/MeasurableSpace/EventuallyMeasurable.lean

Statistics

Metric	Count
Definitions EventuallyMeasurable, EventuallyMeasurableSet, eventuallyMeasurableSpace	3
Theorems comp_eventuallyMeasurable, eventuallyMeasurable, eventuallyMeasurable_of_eventuallyEq, eventuallyMeasurableSet, eventuallyMeasurableSet_of_mem_filter, eventuallyMeasurableSingleton, le_eventuallyMeasurableSpace	7
Total	10

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_eventuallyMeasurable 📖	—	Measurable EventuallyMeasurable	—	—	comp
eventuallyMeasurable 📖	mathematical	Measurable	EventuallyMeasurable	—	le le_eventuallyMeasurableSpace
eventuallyMeasurable_of_eventuallyEq 📖	mathematical	Measurable Filter.EventuallyEq	EventuallyMeasurable	—	EventuallyMeasurable.congr eventuallyMeasurable

MeasurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventuallyMeasurableSet 📖	mathematical	MeasurableSet	EventuallyMeasurableSet	—	Filter.EventuallyEq.refl

(root)

Definitions

Name	Category	Theorems
EventuallyMeasurable 📖	MathDef	2 math math: Measurable.eventuallyMeasurable_of_eventuallyEq, Measurable.eventuallyMeasurable
EventuallyMeasurableSet 📖	MathDef	2 math math: MeasurableSet.eventuallyMeasurableSet, eventuallyMeasurableSet_of_mem_filter
eventuallyMeasurableSpace 📖	CompOp	2 math math: eventuallyMeasurableSingleton, le_eventuallyMeasurableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventuallyMeasurableSet_of_mem_filter 📖	mathematical	Set Filter Filter.instMembership	EventuallyMeasurableSet	—	MeasurableSet.univ Filter.eventuallyEq_univ
eventuallyMeasurableSingleton 📖	mathematical	—	MeasurableSingletonClass eventuallyMeasurableSpace	—	MeasurableSet.eventuallyMeasurableSet MeasurableSet.singleton
le_eventuallyMeasurableSpace 📖	mathematical	—	MeasurableSpace MeasurableSpace.instLE eventuallyMeasurableSpace	—	MeasurableSet.eventuallyMeasurableSet

---

← Back to Index