Commit 2025-09-25 22:03 dd5e2a55

View on Github →

feat(Rel): more API (#26988) Some of this API already exists in Topology.UniformSpace.Defs but not spelled with SetRel, some of it was written for #24173.

Estimated changes

modified theorem SetRel.cod_mono
added theorem SetRel.comp_eq_self
added theorem SetRel.comp_iUnion
added theorem SetRel.comp_sUnion
modified theorem SetRel.dom_mono
added theorem SetRel.iUnion_comp
added theorem SetRel.id_subset
added theorem SetRel.id_subset_iff
added theorem SetRel.inv_eq_self
added theorem SetRel.inv_eq_self_iff
modified theorem SetRel.inv_id
modified theorem SetRel.inv_mono
added theorem SetRel.isRefl_mono
added theorem SetRel.prodMk_mem_comp
added theorem SetRel.prod_comp_prod
added theorem SetRel.sUnion_comp
added theorem SetRel.symmetrize_mono