Partial

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

Statistics

Metric	Count
Definitions PTendsto, PTendsto', RTendsto, RTendsto', pcomap', pmap, rcomap, rcomap', rmap	9
Theorems mem_pmap, mem_rcomap', mem_rmap, pmap_res, ptendsto'_def, ptendsto'_of_ptendsto, ptendsto_def, ptendsto_iff_rtendsto, ptendsto_of_ptendsto', rcomap'_compose, rcomap'_rcomap', rcomap'_sets, rcomap_compose, rcomap_rcomap, rcomap_sets, rmap_compose, rmap_rmap, rmap_sets, rtendsto'_def, rtendsto_def, rtendsto_iff_le_rcomap, tendsto_iff_ptendsto, tendsto_iff_ptendsto_univ, tendsto_iff_rtendsto, tendsto_iff_rtendsto'	25
Total	34

Filter

Definitions

Name	Category	Theorems
PTendsto 📖	MathDef	7 math math: tendsto_iff_ptendsto, ptendsto_nhds, ptendsto_def, tendsto_iff_ptendsto_univ, continuousWithinAt_iff_ptendsto_res, ptendsto_of_ptendsto', ptendsto_iff_rtendsto
PTendsto' 📖	MathDef	4 math math: ptendsto'_of_ptendsto, pcontinuous_iff', ptendsto'_nhds, ptendsto'_def
RTendsto 📖	MathDef	5 math math: rtendsto_def, tendsto_iff_rtendsto, rtendsto_iff_le_rcomap, ptendsto_iff_rtendsto, rtendsto_nhds
RTendsto' 📖	MathDef	3 math math: rtendsto'_nhds, rtendsto'_def, tendsto_iff_rtendsto'
pcomap' 📖	CompOp	—
pmap 📖	CompOp	2 math math: mem_pmap, pmap_res
rcomap 📖	CompOp	4 math math: rcomap_compose, rcomap_sets, rcomap_rcomap, rtendsto_iff_le_rcomap
rcomap' 📖	CompOp	4 math math: rcomap'_compose, rcomap'_rcomap', rcomap'_sets, mem_rcomap'
rmap 📖	CompOp	4 math math: mem_rmap, rmap_compose, rmap_sets, rmap_rmap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_pmap 📖	mathematical	—	Set Filter instMembership pmap PFun.core	—	—
mem_rcomap' 📖	mathematical	—	Set Filter instMembership rcomap' Set.instHasSubset SetRel.preimage	—	—
mem_rmap 📖	mathematical	—	Set Filter instMembership rmap SetRel.core	—	—
pmap_res 📖	mathematical	—	pmap PFun.res map Filter instInf principal	—	ext PFun.core_res
ptendsto'_def 📖	mathematical	—	PTendsto' Set Filter instMembership PFun.preimage	—	rtendsto'_def
ptendsto'_of_ptendsto 📖	mathematical	Set Filter instMembership PFun.Dom PTendsto	PTendsto'	—	ptendsto_def ptendsto'_def PFun.preimage_eq inter_mem
ptendsto_def 📖	mathematical	—	PTendsto Set Filter instMembership PFun.core	—	—
ptendsto_iff_rtendsto 📖	mathematical	—	PTendsto RTendsto PFun.graph'	—	—
ptendsto_of_ptendsto' 📖	mathematical	PTendsto'	PTendsto	—	ptendsto_def ptendsto'_def mem_of_superset PFun.preimage_subset_core
rcomap'_compose 📖	mathematical	—	Filter rcomap' SetRel.comp	—	rcomap'_rcomap'
rcomap'_rcomap' 📖	mathematical	—	rcomap' SetRel.comp	—	ext SetRel.preimage_comp LE.le.trans SetRel.preimage_mono Set.Subset.rfl
rcomap'_sets 📖	mathematical	—	sets rcomap' SetRel.image Set setOf Set.instHasSubset SetRel.preimage	—	—
rcomap_compose 📖	mathematical	—	Filter rcomap SetRel.comp	—	rcomap_rcomap
rcomap_rcomap 📖	mathematical	—	rcomap SetRel.comp	—	filter_eq Set.ext SetRel.core_comp Set.Subset.trans SetRel.core_mono Set.Subset.rfl
rcomap_sets 📖	mathematical	—	sets rcomap SetRel.image Set setOf Set.instHasSubset SetRel.core	—	—
rmap_compose 📖	mathematical	—	Filter rmap SetRel.comp	—	rmap_rmap
rmap_rmap 📖	mathematical	—	rmap SetRel.comp	—	filter_eq SetRel.core_comp
rmap_sets 📖	mathematical	—	sets rmap Set.preimage Set SetRel.core	—	—
rtendsto'_def 📖	mathematical	—	RTendsto' Set Filter instMembership SetRel.preimage	—	Set.Subset.rfl mem_of_superset
rtendsto_def 📖	mathematical	—	RTendsto Set Filter instMembership SetRel.core	—	—
rtendsto_iff_le_rcomap 📖	mathematical	—	RTendsto Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder rcomap	—	rtendsto_def mem_sets mem_of_superset Set.Subset.rfl
tendsto_iff_ptendsto 📖	mathematical	—	Tendsto Filter instInf principal PTendsto PFun.res	—	pmap_res
tendsto_iff_ptendsto_univ 📖	mathematical	—	Tendsto PTendsto PFun.res Set.univ	—	tendsto_iff_ptendsto principal_univ inf_of_le_left
tendsto_iff_rtendsto 📖	mathematical	—	Tendsto RTendsto Function.graph	—	—
tendsto_iff_rtendsto' 📖	mathematical	—	Tendsto RTendsto' Function.graph	—	—

---

← Back to Index