theorem
EmbeddingLike.pairwise_comp
{X : Type u_1}
{Y : Type u_2}
{F : Sort u_3}
[FunLike F Y X]
[EmbeddingLike F Y X]
(f : F)
{p : X → X → Prop}
(h : Pairwise p)
:
Pairwise (Function.onFun p ⇑f)
theorem
EquivLike.pairwise_comp_iff
{X : Type u_1}
{Y : Type u_2}
{F : Sort u_3}
[EquivLike F Y X]
(f : F)
(p : X → X → Prop)
:
Pairwise (Function.onFun p ⇑f) ↔ Pairwise p