mono — Mathlib

English

If x is a maximal P and Q x holds and Q ≤ P, then x is a maximal Q.

Русский

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

LaTeX

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

Lean4

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

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