English
Let hPQ: ∀ ⦃x⦄, Q x → P x and h: ∀ ⦃x⦄, P x → ∃ y, y ≤ x ∧ Q y. Then Minimal P x ↔ Minimal Q x.
Русский
Пусть hPQ: ∀ x, Q x → P x и h: ∀ x, P x → ∃ y, y ≤ x ∧ Q y. Тогда Minimal P x эквивалентно Minimal Q x.
LaTeX
$$$$ (\\forall x\\, (Q x \\to P x)) \\land (\\forall x\\, (P x \\to \\exists y\\,(y \\le x) \\land Q y)) \\;\\Rightarrow\\; (Minimal P x \\iff Minimal Q x). $$$$
Lean4
theorem minimal_iff_minimal_of_imp_of_forall (hPQ : ∀ ⦃x⦄, Q x → P x) (h : ∀ ⦃x⦄, P x → ∃ y, y ≤ x ∧ Q y) :
Minimal P x ↔ Minimal Q x :=
by
refine ⟨fun h' ↦ ⟨?_, fun y hy hyx ↦ h'.le_of_le (hPQ hy) hyx⟩, fun h' ↦ ⟨hPQ h'.prop, fun y hy hyx ↦ ?_⟩⟩
· obtain ⟨y, hyx, hy⟩ := h h'.prop
rwa [((h'.le_of_le (hPQ hy)) hyx).antisymm hyx]
obtain ⟨z, hzy, hz⟩ := h hy
exact (h'.le_of_le hz (hzy.trans hyx)).trans hzy
