Partial

📁 Source: Mathlib/Topology/Partial.lean

Statistics

Metric	Count
Definitions Partial, PContinuous	2
Theorems continuousWithinAt_iff_ptendsto_res, open_dom_of_pcontinuous, pcontinuous_iff', ptendsto'_nhds, ptendsto_nhds, rtendsto'_nhds, rtendsto_nhds	7
Total	9

HahnEmbedding

Definitions

Name	Category	Theorems
Partial 📖	CompOp	2 math math: Partial.lt_extend, Partial.exists_isMax

(root)

Definitions

Name	Category	Theorems
PContinuous 📖	MathDef	1 math math: pcontinuous_iff'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousWithinAt_iff_ptendsto_res 📖	mathematical	—	ContinuousWithinAt Filter.PTendsto PFun.res nhds	—	Filter.tendsto_iff_ptendsto
open_dom_of_pcontinuous 📖	mathematical	PContinuous	IsOpen PFun.Dom	—	PFun.preimage_univ isOpen_univ
pcontinuous_iff' 📖	mathematical	—	PContinuous Filter.PTendsto' nhds	—	PFun.preimage_mono isOpen_iff_nhds Filter.mem_principal Filter.mem_of_superset Filter.ptendsto'_def mem_nhds_iff Set.Subset.refl
ptendsto'_nhds 📖	mathematical	—	Filter.PTendsto' nhds Set Filter Filter.instMembership PFun.preimage	—	rtendsto'_nhds
ptendsto_nhds 📖	mathematical	—	Filter.PTendsto nhds Set Filter Filter.instMembership PFun.core	—	rtendsto_nhds
rtendsto'_nhds 📖	mathematical	—	Filter.RTendsto' nhds Set Filter Filter.instMembership SetRel.preimage	—	Filter.rtendsto'_def all_mem_nhds_filter SetRel.preimage_mono
rtendsto_nhds 📖	mathematical	—	Filter.RTendsto nhds Set Filter Filter.instMembership SetRel.core	—	all_mem_nhds_filter

---

← Back to Index