Uniform separation

This file defines a notion of separation of a set relative to a relation.

For a relation R, an R-separated set s is a set such that every pair of elements of s is R-unrelated.

The concept of uniformly separated sets is used to define two further notions of separation:

• Metric separation: Metric.IsSeparated, defined using the small distance relation.
• Dynamical nets: Dynamics.IsDynNetIn, defined using the dynamical relation.

TODO

• Actually use SetRel.IsSeparated to define the above two notions.
• Link to the notion of separation given by pairwise disjoint balls.

def SetRel.IsSeparated {X : Type u_1} (R : SetRel X X) (s : Set X) : Prop

Given a relation R, a set s is R-separated if its elements are pairwise R-unrelated from each other.

Equations

• R.IsSeparated s = s.Pairwise fun (x y : X) => ¬(x, y) ∈ R

theorem SetRel.IsSeparated.empty {X : Type u_1} {R : SetRel X X} : R.IsSeparated ∅

theorem SetRel.IsSeparated.singleton {X : Type u_1} {R : SetRel X X} {x : X} : R.IsSeparated {x}

@[simp]

theorem SetRel.IsSeparated.of_subsingleton {X : Type u_1} {R : SetRel X X} {s : Set X} (hs : s.Subsingleton) : R.IsSeparated s

theorem Set.Subsingleton.relIsSeparated {X : Type u_1} {R : SetRel X X} {s : Set X} (hs : s.Subsingleton) : R.IsSeparated s

Alias of SetRel.IsSeparated.of_subsingleton.

theorem SetRel.IsSeparated.mono_left {X : Type u_1} {R S : SetRel X X} {s : Set X} (hUV : R ⊆ S) (hs : S.IsSeparated s) : R.IsSeparated s

theorem SetRel.IsSeparated.mono_right {X : Type u_1} {R : SetRel X X} {s t : Set X} (hst : s ⊆ t) (ht : R.IsSeparated t) : R.IsSeparated s

theorem SetRel.isSeparated_insert' {X : Type u_1} {R : SetRel X X} {s : Set X} {x : X} : R.IsSeparated (insert x s) ↔ R.IsSeparated s ∧ (∀ (y : X), y ∈ s → (x, y) ∈ R → x = y) ∧ ∀ (y : X), y ∈ s → (y, x) ∈ R → x = y

theorem SetRel.isSeparated_insert {X : Type u_1} {R : SetRel X X} {s : Set X} {x : X} [R.IsSymm] : R.IsSeparated (insert x s) ↔ R.IsSeparated s ∧ ∀ (y : X), y ∈ s → (x, y) ∈ R → x = y

theorem SetRel.isSeparated_insert_of_notMem {X : Type u_1} {R : SetRel X X} {s : Set X} {x : X} [R.IsSymm] (hx : ¬x ∈ s) : R.IsSeparated (insert x s) ↔ R.IsSeparated s ∧ ∀ (y : X), y ∈ s → ¬(x, y) ∈ R

theorem SetRel.IsSeparated.insert' {X : Type u_1} {R : SetRel X X} {s : Set X} {x : X} (hs : R.IsSeparated s) (h : ∀ (y : X), y ∈ s → (x, y) ∈ R → x = y) (h' : ∀ (y : X), y ∈ s → (y, x) ∈ R → x = y) : R.IsSeparated (insert x s)

theorem SetRel.IsSeparated.insert {X : Type u_1} {R : SetRel X X} {s : Set X} {x : X} [R.IsSymm] (hs : R.IsSeparated s) (h : ∀ (y : X), y ∈ s → (x, y) ∈ R → x = y) : R.IsSeparated (insert x s)