mono — Mathlib

English

If t is partially well-ordered by r and s ⊆ t, then s is partially well-ordered by r as well.

Русский

Если t частично хорошо упорядочено по r и s ⊆ t, то s также частично хорошо упорядочено по r.

LaTeX

$$$(t.PartiallyWellOrderedOn r) \\to (s \\subseteq t) \\to (s.PartiallyWellOrderedOn r)$$$

Lean4

theorem mono (ht : t.PartiallyWellOrderedOn r) (h : s ⊆ t) : s.PartiallyWellOrderedOn r := fun f ↦
  ht (Set.inclusion h ∘ f)

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