eq_empty_relation — Mathlib

English

If a relation r on a type α is irreflexive and α is a singleton, then r equals the empty relation.

Русский

Если отношение r на типе α иррефлексивно и α — единичный тип, то r равно пустому отношению.

LaTeX

$$$\\forall {\\alpha} \\; (r) [IsIrrefl \\\\alpha \\\\; r] [Subsingleton \\alpha], \\; r = EmptyRelation$$$

Lean4

theorem eq_empty_relation (r) [IsIrrefl α r] [Subsingleton α] : r = EmptyRelation :=
  funext₂ <| by simpa using not_rel_of_subsingleton r

Похожие утверждения