instIsTransSubtype — Mathlib

English

If r is transitive, then the induced relation on the subtype p is transitive.

Русский

Если r транзитивно, то ограничение Subrel r p на подптипе p транзитивно.

LaTeX

$$$ \\forall x,y,z\\; (p(x) \\land p(y) \\land p(z) \\land r(x,y) \\land r(y,z)) \\rightarrow r(x,z). $$$

Lean4

instance (r : α → α → Prop) [IsTrans α r] (p : α → Prop) : IsTrans _ (Subrel r p) :=
  ⟨fun x y z => @IsTrans.trans α r _ x y z⟩

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