mem_intent_of_intent_rel — Mathlib

English

If r' x y holds and x belongs to the intent of c', then y belongs to the intent of c'.

Русский

Если r'(x,y) и x принадлежит интенту c', то y принадлежит интенту c'.

LaTeX

$$$[IsTrans\;\alpha\; r']\; \{x,y\in \alpha\},\; r'\,x\,y \land x \in c'.intent \Rightarrow y \in c'.intent$$$

Lean4

theorem mem_intent_of_intent_rel [IsTrans α r'] {x y} (hy : r' x y) (hx : x ∈ c'.intent) : y ∈ c'.intent :=
  by
  rw [← upperPolar_extent]
  exact fun z hz ↦ _root_.trans (rel_extent_intent hz hx) hy

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