Quotients for nested relations

Stream: Is there code for X?

[Patrick Massot]

I was not able to find the following, could someone help me?

import Mathlib.Topology.Constructions


lemma sInf_rel {α : Type*} {S : Set (Setoid α)} {x y : α} :
  (sInf S).Rel x y ↔ ∀ s ∈ S, s.Rel x y := Iff.rfl

lemma quotient_mk_sInf_eq {α : Type*} {S : Set (Setoid α)} {x y : α} :
    Quotient.mk (sInf S) x = Quotient.mk (sInf S) y ↔ ∀ s ∈ S, s.Rel x y := by
  simp
  rfl

def Setoid.map_of_le {α : Type*} {s t : Setoid α} (h : s ≤ t) : Quotient s → Quotient t :=
  Quotient.map' id h

def Setoid.map_sInf {α : Type*} {S : Set (Setoid α)} {s : Setoid α} (h : s ∈ S) :
    Quotient (sInf S) → Quotient s :=
  Setoid.map_of_le fun _ _ a ↦ a s h

lemma continuous_map_of_le {α : Type*} [TopologicalSpace α]
    {s t : Setoid α} (h : s ≤ t) : Continuous (Setoid.map_of_le h) :=
  continuous_coinduced_rng

lemma continuous_map_sInf {α : Type*} [TopologicalSpace α]
    {S : Set (Setoid α)} {s : Setoid α} (h : s ∈ S) : Continuous (Setoid.map_sInf h) :=
  continuous_coinduced_rng

[Patrick Massot]

Anyone for that one? @Yaël Dillies maybe knows the first four declarations?

[Yaël Dillies]

Looking around docs#Setoid.top_def, your first lemma indeed seems to be missing. Your second lemma is a bit weird, no? Your Setoid.map_of_le is a special case (although not very practically so) of docs#Setoid.mapOfSurjective

[Yaël Dillies]

Also, nifty! You found out that Yaëlbot is not online 24/7 :grinning:

[Eric Wieser]

Your first lemma is closest to docs#Setoid.sInf_def, with some disagreement about a normal form.