Separated

📁 Source: Mathlib/Data/Rel/Separated.lean

Statistics

Metric	Count
Definitions IsSeparated	1
Theorems relIsSeparated, empty, insert, insert', mono_left, mono_right, of_subsingleton, singleton, isSeparated_insert, isSeparated_insert', isSeparated_insert_of_notMem	11
Total	12

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
relIsSeparated 📖	mathematical	Set.Subsingleton	SetRel.IsSeparated	—	SetRel.IsSeparated.of_subsingleton

SetRel

Definitions

Name	Category	Theorems
IsSeparated 📖	MathDef	8 math math: Metric.isSeparated_iff_setRelIsSeparated, isSeparated_insert', IsSeparated.of_subsingleton, IsSeparated.empty, Set.Subsingleton.relIsSeparated, IsSeparated.singleton, isSeparated_insert_of_notMem, isSeparated_insert

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparated_insert 📖	mathematical	—	IsSeparated Set Set.instInsert	—	Set.pairwise_insert_of_symmetric symm
isSeparated_insert' 📖	mathematical	—	IsSeparated Set Set.instInsert	—	not_imp_comm
isSeparated_insert_of_notMem 📖	mathematical	Set Set.instMembership	IsSeparated Set.instInsert SetRel	—	Set.pairwise_insert_of_symmetric_of_notMem symm

SetRel.IsSeparated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
empty 📖	mathematical	—	SetRel.IsSeparated Set Set.instEmptyCollection	—	Set.pairwise_empty
insert 📖	mathematical	SetRel.IsSeparated	Set Set.instInsert	—	SetRel.isSeparated_insert
insert' 📖	mathematical	SetRel.IsSeparated	Set Set.instInsert	—	SetRel.isSeparated_insert'
mono_left 📖	—	SetRel Set.instHasSubset SetRel.IsSeparated	—	—	Set.Pairwise.mono'
mono_right 📖	—	Set Set.instHasSubset SetRel.IsSeparated	—	—	Set.Pairwise.mono
of_subsingleton 📖	mathematical	Set.Subsingleton	SetRel.IsSeparated	—	Set.Subsingleton.pairwise
singleton 📖	mathematical	—	SetRel.IsSeparated Set Set.instSingletonSet	—	Set.pairwise_singleton

---

← Back to Index