set

📁 Source: MathlibTest/grind/set.lean

Statistics

Metric	Count
Definitions set, set, set, set, set, set, set	7
Theorems set, set, set, set, set	5
Total	12

HNNExtension.NormalWord.TransversalPair

Definitions

Name	Category	Theorems
set 📖	CompOp	3 math math: HNNExtension.NormalWord.mem_set, HNNExtension.NormalWord.unitsSMulGroup_snd, compl

Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
set 📖	mathematical	—	Infinite Set	—	of_injective Set.singleton_injective

IsAddUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
set 📖	mathematical	IsAddUnit	Set Set.addMonoid Set.instSingletonSet	—	map AddMonoidHom.instAddMonoidHomClass

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
set 📖	mathematical	IsUnit	Set Set.monoid Set.instSingletonSet	—	map MonoidHom.instMonoidHomClass

List.Nodup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
set 📖	—	—	—	—	of_cons

List.Vector

Definitions

Name	Category	Theorems
set 📖	CompOp	8 math math: sum_set, get_set_same, prod_set, sum_set', toList_set, prod_set', get_set_eq_if, get_set_of_ne

MeasureTheory.Measure.FiniteSpanningSetsIn

Definitions

Name	Category	Theorems
set 📖	CompOp	5 math math: spanning, finite, MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn, disjointed_set_eq, set_mem

MeasureTheory.closedCompactCylinders

Definitions

Name	Category	Theorems
set 📖	CompOp	3 math math: isCompact, eq_cylinder, isClosed

MeasureTheory.measurableCylinders

Definitions

Name	Category	Theorems
set 📖	CompOp	2 math math: eq_cylinder, measurableSet

Monoid.PushoutI.NormalWord.Transversal

Definitions

Name	Category	Theorems
set 📖	CompOp	6 math math: compl, one_mem, Monoid.PushoutI.NormalWord.cons_head, Monoid.PushoutI.NormalWord.Pair.normalized, Monoid.PushoutI.NormalWord.normalized, Monoid.PushoutI.NormalWord.cons_toList

Stream'.Seq

Definitions

Name	Category	Theorems
set 📖	CompOp	7 math math: set_cons_succ, get?_set_of_not_terminatedAt, set_nil, get?_set_of_terminatedAt, drop_set_of_lt, set_cons_zero, get?_set_of_ne

TopologicalSpace.NoetherianSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
set 📖	mathematical	—	TopologicalSpace.NoetherianSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	Topology.IsInducing.noetherianSpace Topology.IsInducing.subtypeVal

---

← Back to Index