Complements and transitive closure of relations as sets of pairs

[UPSTREAM] supplements to Mathlib/Basic/Rel.lean. The core and the preimage of a relation are dual under complement (SetRel.core_compl, SetRel.preimage_compl), the core is antitone in the relation (SetRel.core_subset_core_left) and sends unions to intersections (SetRel.core_iUnion), and the transitive closure of a relation (SetRel.transGen) has as core the intersection of the iterated cores (SetRel.core_transGen).

Main definitions

• SetRel.ofSuccessors: a set-valued function α → Set β as a relation, whose core at a is inclusion of f a (SetRel.mem_core_ofSuccessors) and whose image is the union of the values (SetRel.image_ofSuccessors).
• SetRel.transGen: the transitive closure of R : SetRel α α, Relation.TransGen of its pointwise relation.

Complements

theorem SetRel.core_compl {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t : Set β) : R.core tᶜ = (R.preimage t)ᶜ

theorem SetRel.preimage_compl {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t : Set β) : R.preimage tᶜ = (R.core t)ᶜ

theorem SetRel.core_iUnion {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (R : ι → SetRel α β) (t : Set β) : core (⋃ (i : ι), R i) t = ⋂ (i : ι), (R i).core t

The core along a union of relations is the intersection of the cores.

theorem SetRel.core_subset_core_left {α : Type u_1} {β : Type u_2} {R₁ R₂ : SetRel α β} {t : Set β} (h : R₁ ⊆ R₂) : R₂.core t ⊆ R₁.core t

Restricting the relation enlarges the core.

instance SetRel.isRefl_id {α : Type u_1} : SetRel.id.IsRefl

Decidability over finite codomains

@[instance_reducible]

instance SetRel.instDecidableMemSetCoreOfFintypeOfProdMkOfDecidablePred_linglib {α : Type u_1} {β : Type u_2} [Fintype β] (R : SetRel α β) (t : Set β) (a : α) [(b : β) → Decidable ((a, b) ∈ R)] [DecidablePred fun (x : β) => x ∈ t] : Decidable (a ∈ R.core t)

Equations

• R.instDecidableMemSetCoreOfFintypeOfProdMkOfDecidablePred_linglib t a = decidable_of_iff (∀ (b : β), (a, b) ∈ R → b ∈ t) ⋯

@[instance_reducible]

instance SetRel.instDecidableMemSetPreimageOfFintypeOfProdMkOfDecidablePred_linglib {α : Type u_1} {β : Type u_2} [Fintype β] (R : SetRel α β) (t : Set β) (a : α) [(b : β) → Decidable ((a, b) ∈ R)] [DecidablePred fun (x : β) => x ∈ t] : Decidable (a ∈ R.preimage t)

Equations

• R.instDecidableMemSetPreimageOfFintypeOfProdMkOfDecidablePred_linglib t a = decidable_of_iff (∃ b ∈ t, (a, b) ∈ R) ⋯

Relations from set-valued functions

def SetRel.ofSuccessors {α : Type u_1} {β : Type u_2} (f : α → Set β) : SetRel α β

A set-valued function as a relation, relating a to every member of f a.

Equations

• SetRel.ofSuccessors f = {p : α × β | p.2 ∈ f p.1}

@[simp]

theorem SetRel.mem_ofSuccessors {α : Type u_1} {β : Type u_2} {a : α} {f : α → Set β} {y : β} : (a, y) ∈ ofSuccessors f ↔ y ∈ f a

theorem SetRel.mem_core_ofSuccessors {α : Type u_1} {β : Type u_2} {t : Set β} {a : α} {f : α → Set β} : a ∈ (ofSuccessors f).core t ↔ f a ⊆ t

theorem SetRel.image_ofSuccessors {α : Type u_1} {β : Type u_2} (f : α → Set β) (s : Set α) : (ofSuccessors f).image s = ⋃ a ∈ s, f a

theorem SetRel.mem_preimage_ofSuccessors {α : Type u_1} {β : Type u_2} {t : Set β} {a : α} {f : α → Set β} : a ∈ (ofSuccessors f).preimage t ↔ (f a ∩ t).Nonempty

Transitive closure

def SetRel.transGen {α : Type u_1} (R : SetRel α α) : SetRel α α

The transitive closure of a relation.

Equations

• R.transGen = {p : α × α | Relation.TransGen (fun (x1 x2 : α) => (x1, x2) ∈ R) p.1 p.2}

@[simp]

theorem SetRel.mem_transGen {α : Type u_1} {a b : α} {R : SetRel α α} : (a, b) ∈ R.transGen ↔ Relation.TransGen (fun (x1 x2 : α) => (x1, x2) ∈ R) a b

theorem SetRel.subset_transGen {α : Type u_1} {R : SetRel α α} : R ⊆ R.transGen

instance SetRel.instIsTransTransGen {α : Type u_1} {R : SetRel α α} : R.transGen.IsTrans

theorem SetRel.core_transGen_subset_core {α : Type u_1} {R : SetRel α α} {s : Set α} : R.transGen.core s ⊆ R.core s

theorem SetRel.core_transGen {α : Type u_1} {R : SetRel α α} {s : Set α} : R.transGen.core s = ⋂ (n : ℕ), R.core^[n + 1] s

The core of the transitive closure is the intersection of the iterated cores.