BoolIndicator

📁 Source: Mathlib/Data/Set/BoolIndicator.lean

Statistics

Metric	Count
Definitions boolIndicator	1
Theorems mem_iff_boolIndicator, notMem_iff_boolIndicator, preimage_boolIndicator, preimage_boolIndicator_eq_union, preimage_boolIndicator_false, preimage_boolIndicator_true	6
Total	7

Set

Definitions

Name	Category	Theorems
boolIndicator 📖	CompOp	6 math, 2 bridge math: continuousOn_boolIndicator_iff_isClopen, preimage_boolIndicator, preimage_boolIndicator_eq_union, preimage_boolIndicator_true, continuous_boolIndicator_iff_isClopen, preimage_boolIndicator_false bridge: mem_iff_boolIndicator, notMem_iff_boolIndicator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_iff_boolIndicator 📖	bridging (iff)	—	Set instMembership boolIndicator	boolIndicator	—
notMem_iff_boolIndicator 📖	bridging (iff)	—	Set instMembership boolIndicator	boolIndicator	—
preimage_boolIndicator 📖	mathematical	—	preimage boolIndicator univ Compl.compl Set instCompl instEmptyCollection	—	preimage_boolIndicator_eq_union union_compl_self union_empty empty_union union_self
preimage_boolIndicator_eq_union 📖	mathematical	—	preimage boolIndicator Set instUnion instMembership instEmptyCollection Compl.compl instCompl	—	ext union_compl_self union_empty empty_union union_self
preimage_boolIndicator_false 📖	mathematical	—	preimage boolIndicator Set instSingletonSet Compl.compl instCompl	—	ext notMem_iff_boolIndicator
preimage_boolIndicator_true 📖	mathematical	—	preimage boolIndicator Set instSingletonSet	—	ext mem_iff_boolIndicator

---

← Back to Index