Setoid quotient helpers

This file records small generic additions to Mathlib's Setoid quotient API.

Main declarations

• TauCeti.Setoid.map_of_le_mk: the quotient map induced by a setoid inequality sends a representative to the same representative in the larger quotient.

@[simp]

theorem TauCeti.Setoid.map_of_le_mk {α : Type u_1} {s t : Setoid α} (h : s ≤ t) (x : α) : Setoid.map_of_le h (Quotient.mk'' x) = Quotient.mk'' x

The quotient map induced by a setoid inequality sends a representative to the same representative in the larger quotient.