mono — Mathlib

English

If Minimal P x holds, and Q is contained in P, and Q x holds, then Minimal Q x holds.

Русский

Если x минимален относительно P и Q ⊆ P, а Q x верно, то x минимален относительно Q.

LaTeX

$$$\\text{Minimal } P\\, x \\to (\\forall y, Q(y) \\to P(y)) \\to Q(x) \\to \\text{Minimal } Q\\, x$$$

Lean4

theorem mono (h : Minimal P x) (hle : Q ≤ P) (hQ : Q x) : Minimal Q x :=
  ⟨hQ, fun y hQy ↦ h.le_of_le (hle y hQy)⟩

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