Documentation Verification Report

Indicator

📁 Source: Mathlib/Topology/Algebra/Indicator.lean

Statistics

Metric	Count
Definitions	0
Theorems `indicator`, `mulIndicator`, `continuousAt_indicator`, `continuousAt_mulIndicator`, `continuous_indicator`, `continuous_mulIndicator`, `continuous_indicator`, `continuous_mulIndicator`	8
Total	8

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`indicator` 📖	mathematical	`Continuous`	`Set.indicator`	—	`piecewise` `continuous_const`
`mulIndicator` 📖	mathematical	`Continuous`	`Set.mulIndicator`	—	`piecewise` `continuous_const`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_indicator` 📖	mathematical	`ContinuousOn` `interior` `Set` `Set.instMembership` `frontier`	`ContinuousAt` `Set.indicator`	—	`compl_frontier_eq_union_interior` `Set.mem_compl_iff` `mem_interior_iff_mem_nhds` `interior_interior` `ContinuousAt.congr` `continuousAt` `Filter.eventuallyEq_iff_exists_mem` `Set.EqOn.mono` `interior_subset` `Set.EqOn.symm` `Set.eqOn_indicator` `continuousAt_const` `Set.eqOn_indicator'`
`continuousAt_mulIndicator` 📖	mathematical	`ContinuousOn` `interior` `Set` `Set.instMembership` `frontier`	`ContinuousAt` `Set.mulIndicator`	—	`compl_frontier_eq_union_interior` `Set.mem_compl_iff` `mem_interior_iff_mem_nhds` `interior_interior` `ContinuousAt.congr` `continuousAt` `Filter.eventuallyEq_iff_exists_mem` `Set.EqOn.mono` `interior_subset` `Set.EqOn.symm` `Set.eqOn_mulIndicator` `continuousAt_const` `Set.eqOn_mulIndicator'`

IsClopen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_indicator` 📖	mathematical	`IsClopen` `Continuous`	`Set.indicator`	—	`Continuous.indicator` `isClopen_iff_frontier_eq_empty` `Set.mem_empty_iff_false` `IsEmpty.forall_iff` `instIsEmptyFalse`
`continuous_mulIndicator` 📖	mathematical	`IsClopen` `Continuous`	`Set.mulIndicator`	—	`Continuous.mulIndicator` `isClopen_iff_frontier_eq_empty` `instIsEmptyFalse`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_indicator` 📖	mathematical	`ContinuousOn` `closure`	`Continuous` `Set.indicator`	—	`continuous_piecewise` `continuousOn_const`
`continuous_mulIndicator` 📖	mathematical	`ContinuousOn` `closure`	`Continuous` `Set.mulIndicator`	—	`continuous_piecewise` `continuousOn_const`

---

← Back to Index