Theorems · Theorem · logic and foundations

EmbeddingLike.pairwise_comp

∀ {X : Type u_1} {Y : Type u_2} {F : Sort u_3} [inst : FunLike F Y X] [EmbeddingLike F Y X] (f : F) {p : X → X → Prop},
  Pairwise p → Pairwise (Function.onFun p ⇑f)

Defined in

Mathlib.Logic.Equiv.Pairwise

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

FunLikeEmbeddingLike