mem_extent_of_rel_extent — Mathlib

English

If r' y x holds and x lies in the extent of c', then y lies in the extent of c'.

Русский

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

LaTeX

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

Lean4

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

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