eqvGen_le — Mathlib

English

The equivalence closure of a binary relation r is contained in any equivalence relation containing r.

Русский

Замыкание по эквивалентности для бинарного отношения r содержится в любом отношении эквивалентности, содержащем r.

LaTeX

$$$$ \\mathrm{EqvGen.setoid}(r) \\le s \\quad\\text{if }\\ \\forall x,y,\\ r x y \\to s x y. $$$$

Lean4

/-- The equivalence closure of a binary relation r is contained in any equivalence
relation containing r. -/
theorem eqvGen_le {r : α → α → Prop} {s : Setoid α} (h : ∀ x y, r x y → s x y) : EqvGen.setoid r ≤ s := by
  rw [eqvGen_eq]; exact sInf_le h

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