Theorem Relation.bicompl_map_bicompl_eq_bicompl

Modification history

2026-09-10 16:50
Mathlib/Logic/Relation.lean
feat(Logic/Relation): `Map r f g ≤ s ↔ r ≤ s.bicompl f g` (#38432) …
Added Relation.bicompl_map_bicompl_eq_bicomplView on Github →