maximal_iff_maximal_of_imp_of_forall

English

Let hPQ: ∀ ⦃x⦄, Q x → P x and h: ∀ ⦃x⦄, P x → ∃ y, x ≤ y ∧ Q y. Then Maximal P x ↔ Maximal Q x.

Русский

Пусть hPQ: ∀ x, Q x → P x и h: ∀ x, P x → ∃ y, x ≤ y ∧ Q y. Тогда Maximal P x эквивалентно Maximal Q x.

LaTeX

$$$$ (\\forall x\\, (Q x \\to P x)) \\land (\\forall x\\, (P x \\to \\exists y\\,(x \\le y) \\land Q y)) \\;\\Rightarrow\\; (Maximal P x \\iff Maximal Q x). $$$$

Lean4

theorem maximal_iff_maximal_of_imp_of_forall (hPQ : ∀ ⦃x⦄, Q x → P x) (h : ∀ ⦃x⦄, P x → ∃ y, x ≤ y ∧ Q y) :
    Maximal P x ↔ Maximal Q x :=
  minimal_iff_minimal_of_imp_of_forall (α := αᵒᵈ) hPQ h

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