disjoint_extent_intent — Mathlib

English

For any concept c' and an irreflexive relation r', the extent and intent are disjoint.

Русский

Для любого концепта c' и иррефлексивного отношения r' экстент и интент непересекаются.

LaTeX

$$$[IsIrrefl\;\alpha\; r'] \Rightarrow \mathrm{Disjoint}(c'.extent, c'.intent)$$$

Lean4

/-- Note that if `r'` is the `≤` relation, this theorem will often not be true! -/
theorem disjoint_extent_intent [IsIrrefl α r'] : Disjoint c'.extent c'.intent :=
  by
  rw [disjoint_iff_forall_ne]
  rintro x hx _ hx' rfl
  exact irrefl x (rel_extent_intent hx hx')

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