reflGen_minimal — Mathlib

English

If r' is reflexive and contains r, then ReflGen r x y implies r' x y for any x,y.

Русский

Если r' рефлексивно и содержит r, то из ReflGen r x y следует r' x y.

LaTeX

$$$ \forall {α} {r r' : α \to α \to \mathrm{Prop}}, \text{Reflexive } r' \to (\forall x y, r x y \to r' x y) \to \forall {x y}, \mathrm{ReflGen} r x y \to r' x y $$$

Lean4

theorem reflGen_minimal {r' : α → α → Prop} (hr' : Reflexive r') (h : ∀ x y, r x y → r' x y) {x y : α}
    (hxy : ReflGen r x y) : r' x y := by simpa [reflGen_eq_self hr'] using ReflGen.mono h hxy

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