mono — Mathlib

English

If t is a subset of s and s is pairwise with respect to a relation r, then t is pairwise with respect to r.

Русский

Если t ⊆ s и s попарно по отношению r, то и t попарно по отношению r.

LaTeX

$$$\forall {\alpha} {r : \alpha \to \alpha \to \mathrm{Prop}} {s t : Set \alpha}, t \subseteq s \to s.Pairwise r \to t.Pairwise r$$$

Lean4

theorem mono (h : t ⊆ s) (hs : s.Pairwise r) : t.Pairwise r := fun _x xt _y yt => hs (h xt) (h yt)

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