English
A variant form of forall_of_forall_prime with an alternative maximality condition.
Русский
Вариант forall_of_forall_prime с другой формулировкой максимальности.
LaTeX
$$Variant of forall_of_forall_prime$$
Lean4
/-- A variant of `forall_of_forall_prime` with a different spelling of the condition `hmax`. -/
theorem forall_of_forall_prime' (hchain : ∀ C ⊆ {I | ¬P I}, IsChain (· ≤ ·) C → ∀ _ ∈ C, P (sSup C) → ∃ I ∈ C, P I)
(hprime : ∀ I, I.IsPrime → P I) : ∀ I, P I :=
by
refine forall_of_forall_prime hP (fun I hI ↦ ?_) hprime
obtain ⟨M, _, hM⟩ : ∃ M, I ≤ M ∧ Maximal (¬P ·) M :=
by
refine zorn_le_nonempty₀ {I | ¬P I} (fun C hC₁ hC₂ J hJ ↦ ⟨sSup C, ?_, fun _ ↦ le_sSup⟩) I hI
intro H
obtain ⟨_, h₁, h₂⟩ := hchain C hC₁ hC₂ J hJ H
exact hC₁ h₁ h₂
exact ⟨M, hM⟩
