maximal_and_iff_left_of_imp — Mathlib

English

Let P and Q be predicates on a preorder, with P(x) → Q(x) for all x. Then Maximal (Q x ∧ P x) x is equivalent to Q x ∧ Maximal P x.

Русский

Пусть P и Q — предикаты на порядковом множестве, причём P(x) → Q(x) для всех x. Тогда Maximal (Q x ∧ P x) x эквивалентно Q x ∧ Maximal P x.

LaTeX

$$$ (\forall {x}, P x \rightarrow Q x) \rightarrow \bigl( \operatorname{Maximal}(\lambda x . Q x \land P x) x \leftrightarrow Q x \land \operatorname{Maximal}(\lambda x . P x) x \bigr) $$$

Lean4

theorem maximal_and_iff_left_of_imp (hPQ : ∀ ⦃x⦄, P x → Q x) : Maximal (fun x ↦ Q x ∧ P x) x ↔ Q x ∧ (Maximal P x) :=
  minimal_and_iff_left_of_imp (α := αᵒᵈ) hPQ

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