exists_minimal_le_of_wellFoundedLT

English

Let P be a predicate and a be such that P a holds; then there exists b ≤ a with Minimal P b.

Русский

Пусть P — предикат и дано a так, что P a истина; тогда существует b ≤ a с Minimal P b.

LaTeX

$$$ \forall {P a}, P a \rightarrow \exists b \le a, \operatorname{Minimal} P b $$$

Lean4

theorem exists_minimal_le_of_wellFoundedLT (P : α → Prop) (a : α) (ha : P a) : ∃ b ≤ a, Minimal P b :=
  by
  obtain ⟨b, ⟨hba, hb⟩, hbmin⟩ := exists_minimal_of_wellFoundedLT (fun b ↦ b ≤ a ∧ P b) ⟨a, le_rfl, ha⟩
  exact ⟨b, hba, hb, fun c hc hcb ↦ hbmin ⟨hcb.trans hba, hc⟩ hcb⟩

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