ExtendFrom

📁 Source: Mathlib/Topology/ExtendFrom.lean

Statistics

Metric	Count
Definitions extendFrom	1
Theorems continuousOn_extendFrom, continuous_extendFrom, extendFrom_eq, extendFrom_extends, tendsto_extendFrom	5
Total	6

(root)

Definitions

Name	Category	Theorems
extendFrom 📖	CompOp	13 math math: continuous_extendFrom, continuousOn_Icc_extendFrom_Ioo, eq_lim_at_right_extendFrom_uIoo, extendFrom_extends, eq_lim_at_left_extendFrom_uIoo, continuousOn_extendFrom, continuousOn_uIcc_extendFrom_uIoo, eq_lim_at_right_extendFrom_Ioo, eq_lim_at_left_extendFrom_Ioo, tendsto_extendFrom, continuousOn_Ioc_extendFrom_Ioo, continuousOn_Ico_extendFrom_Ioo, extendFrom_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_extendFrom 📖	mathematical	Set Set.instHasSubset closure Filter.Tendsto nhdsWithin nhds	ContinuousOn extendFrom	—	tendsto_extendFrom Filter.HasBasis.tendsto_left_iff nhdsWithin_basis_open IsOpen.mem_nhds Set.inter_comm inter_mem_nhdsWithin IsClosed.mem_of_tendsto mem_closure_iff_nhdsWithin_neBot Filter.mem_of_superset Filter.inter_mem_inf Filter.mem_principal_self Filter.HasBasis.tendsto_right_iff closed_nhds_basis
continuous_extendFrom 📖	mathematical	Dense Filter.Tendsto nhdsWithin nhds	Continuous extendFrom	—	continuousOn_univ continuousOn_extendFrom
extendFrom_eq 📖	mathematical	Set Set.instMembership closure Filter.Tendsto nhdsWithin nhds	extendFrom	—	tendsto_nhds_unique mem_closure_iff_nhdsWithin_neBot tendsto_nhds_limUnder
extendFrom_extends 📖	mathematical	ContinuousOn Set Set.instMembership	extendFrom	—	extendFrom_eq subset_closure
tendsto_extendFrom 📖	mathematical	Filter.Tendsto nhdsWithin nhds	extendFrom	—	tendsto_nhds_limUnder

---

← Back to Index