chain_mono — Mathlib

English

The function assigning to a relation the corresponding Cycle predicate is monotone in the relation parameter.

Русский

Функция, сопоставляющая отношение и соответствующую цепь, монотонна по отношению к этому отношению.

LaTeX

$$$$ \\text{theorem chain\\_mono: Monotone (Chain : (\\alpha \\to \\alpha \\to Prop) \\to Cycle \\alpha \\to Prop).} $$$$

Lean4

/-- As a function from a relation to a predicate, `chain` is monotonic. -/
theorem chain_mono : Monotone (Chain : (α → α → Prop) → Cycle α → Prop) := fun _a _b hab _s => Chain.imp hab

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