rel_extent_intent — Mathlib

English

If x lies in the extent of a concept c and y lies in the intent of c, then r(x,y) holds.

Русский

Если x принадлежит экстенту концепта c, а y принадлежит интенту c, то выполняется отношение r(x,y).

LaTeX

$$$\forall x \in \alpha, \forall y \in \beta, \; x \in c.extent \land y \in c.intent \rightarrow r\,x\,y$$$

Lean4

theorem rel_extent_intent {x y} (hx : x ∈ c.extent) (hy : y ∈ c.intent) : r x y :=
  by
  rw [← c.upperPolar_extent] at hy
  exact hy hx

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