eqvGen_mono — Mathlib

English

Equivalence closure is monotone: if r x y implies s x y, then EqvGen.setoid r ≤ EqvGen.setoid s.

Русский

Замыкание по эквивалентности монотонно: если r x y ⇒ s x y, то EqvGen.setoid r ≤ EqvGen.setoid s.

LaTeX

$$$$ eqvGen\\_mono\\!\\{r s : α \\to α \\to Prop\\} (h : \\forall x y, r x y \\to s x y) : EqvGen.setoid r ≤ EqvGen.setoid s. $$$$

Lean4

/-- Equivalence closure of binary relations is monotone. -/
theorem eqvGen_mono {r s : α → α → Prop} (h : ∀ x y, r x y → s x y) : EqvGen.setoid r ≤ EqvGen.setoid s :=
  eqvGen_le fun _ _ hr => EqvGen.rel _ _ <| h _ _ hr

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