codisjoint_extent_intent — Mathlib

English

Under suitable trichotomy and transitivity assumptions on r', the pair c'.extent and c'.intent are codisjoint.

Русский

При соответствующих гипотезах трёхчленного и транзитивного характера r' пары экстент и интент концепта кодисожины.

LaTeX

$$$[IsTrichotomous\;\alpha\; r']\,[IsTrans\;\alpha\; r'] : \mathrm{Codisjoint}(c'.extent, c'.intent)$$$

Lean4

theorem codisjoint_extent_intent [IsTrichotomous α r'] [IsTrans α r'] : Codisjoint c'.extent c'.intent :=
  by
  rw [codisjoint_iff_le_sup]
  refine fun x _ ↦ or_iff_not_imp_left.2 fun hx ↦ ?_
  rw [← upperPolar_extent]
  intro y hy
  obtain h | rfl | h := trichotomous_of r' x y
  · cases hx <| mem_extent_of_rel_extent h hy
  · contradiction
  · assumption

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