RelHomClass.isIrrefl

Deprecated since 2026-01-07Use RelHomClass.irrefl instead.

∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_5} [inst : FunLike F α β]
  [RelHomClass F r s] (f : F) [Std.Irrefl s], Std.Irrefl r

Alias of RelHomClass.irrefl.

Defined in: Mathlib.Order.RelIso.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 7 from the axioms · uses no axioms
Assumes: FunLike RelHomClass Std.Irrefl

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

FunLikestatement · cited by 2,560
RelHomClassstatement · cited by 13
RelHomClass.irreflproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.