Piecewise

📁 Source: Mathlib/Topology/Piecewise.lean

Statistics

Metric	Count
Definitions	0
Theorems if, if_const, piecewise, if, if', piecewise, piecewise', ite, ite', continuousAt_update_same, continuousOn_piecewise_ite, continuousOn_piecewise_ite', continuousWithinAt_update_same, continuous_if, continuous_if', continuous_if_const, continuous_piecewise, ite_inter_closure_compl_eq_of_inter_frontier_eq, ite_inter_closure_eq_of_inter_frontier_eq	19
Total	19

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
if 📖	—	Continuous	—	—	continuous_if continuousOn
if_const 📖	—	Continuous	—	—	continuous_if_const
piecewise 📖	mathematical	Continuous	Set.piecewise	—	if

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
if 📖	—	ContinuousOn Set Set.instInter closure setOf	—	—	if' tendsto_nhdsWithin_mono_left Set.inter_subset_inter_right subset_closure closure_compl Set.mem_compl_iff mono
if' 📖	—	Filter.Tendsto nhdsWithin Set Set.instInter setOf nhds ContinuousOn	—	—	Filter.Tendsto.piecewise_nhdsWithin Set.inter_univ Set.union_compl_self Set.inter_union_distrib_left ContinuousWithinAt.union ContinuousWithinAt.congr subset_closure closure_compl continuousWithinAt_of_notMem_closure closure_inter_subset_inter_closure interior_subset
piecewise 📖	mathematical	ContinuousOn Set Set.instInter closure Compl.compl Set.instCompl	Set.piecewise	—	if
piecewise' 📖	—	Filter.Tendsto nhdsWithin Set Set.instInter nhds Set.piecewise Compl.compl Set.instCompl ContinuousOn	—	—	if'

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ite 📖	mathematical	IsOpen Set Set.instInter frontier	Set.ite	—	ite' Set.ext_iff
ite' 📖	mathematical	IsOpen Set Set.instMembership	Set.ite	—	Set.piecewise_eq_of_mem Set.piecewise_eq_of_notMem continuous_piecewise Continuous.continuousOn

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt_update_same 📖	mathematical	—	ContinuousAt Function.update Filter.Tendsto nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet nhds	—	continuousWithinAt_univ continuousWithinAt_update_same Set.compl_eq_univ_diff
continuousOn_piecewise_ite 📖	mathematical	ContinuousOn Set Set.instInter frontier Set.EqOn	Set.piecewise Set.ite	—	continuousOn_piecewise_ite' ContinuousOn.mono Set.inter_subset_left
continuousOn_piecewise_ite' 📖	mathematical	ContinuousOn Set Set.instInter closure Compl.compl Set.instCompl frontier Set.EqOn	Set.piecewise Set.ite	—	ContinuousOn.piecewise Set.ite_inter_of_inter_eq ite_inter_closure_eq_of_inter_frontier_eq ite_inter_closure_compl_eq_of_inter_frontier_eq
continuousWithinAt_update_same 📖	mathematical	—	ContinuousWithinAt Function.update Filter.Tendsto nhdsWithin Set Set.instSDiff Set.instSingletonSet nhds	—	continuousWithinAt_diff_self ContinuousWithinAt.eq_1 Function.update_self Filter.tendsto_congr' eventually_nhdsWithin_iff Filter.Eventually.of_forall Function.update_of_ne
continuous_if 📖	mathematical	ContinuousOn closure setOf	Continuous	—	continuousOn_univ ContinuousOn.if Set.univ_inter
continuous_if' 📖	mathematical	Filter.Tendsto nhdsWithin setOf nhds ContinuousOn	Continuous	—	continuousOn_univ ContinuousOn.if' Set.univ_inter
continuous_if_const 📖	—	Continuous	—	—	—
continuous_piecewise 📖	mathematical	ContinuousOn closure Compl.compl Set Set.instCompl	Continuous Set.piecewise	—	continuous_if
ite_inter_closure_compl_eq_of_inter_frontier_eq 📖	mathematical	Set Set.instInter frontier	Set.ite closure Compl.compl Set.instCompl	—	Set.ite_compl ite_inter_closure_eq_of_inter_frontier_eq frontier_compl
ite_inter_closure_eq_of_inter_frontier_eq 📖	mathematical	Set Set.instInter frontier	Set.ite closure	—	closure_eq_self_union_frontier Set.inter_union_distrib_left Set.ite_inter_self Set.ite_inter_of_inter_eq

---

← Back to Index