English
Let P and Q be predicates on a preorder and assume P(x) implies Q(x) for every x. Then x is a maximal element for the conjunction P(x) ∧ Q(x) if and only if x is maximal for P(x) and Q(x) holds.
Русский
Пусть P и Q — предикаты на порядковом множестве и предположим, что P(x) ⇒ Q(x) для каждого x. Тогда x максимально по отношению к объединению P(x) ∧ Q(x) тогда и только тогда, когда x максимально по P(x) и выполнено Q(x).
LaTeX
$$$ (\forall {x}, P x \rightarrow Q x) \rightarrow \bigl( \operatorname{Maximal}(\lambda x . P x \land Q x) x \leftrightarrow ( \operatorname{Maximal}(\lambda x . P x) x) \land Q x \bigr) $$$
Lean4
theorem maximal_and_iff_right_of_imp (hPQ : ∀ ⦃x⦄, P x → Q x) : Maximal (fun x ↦ P x ∧ Q x) x ↔ (Maximal P x) ∧ Q x :=
minimal_and_iff_right_of_imp (α := αᵒᵈ) hPQ
