exists_minimal — Mathlib

English

There exists a minimal Solution in the family; i.e., some S1 with isMinimal property.

Русский

Существует минимальное решение в семействе решений.

LaTeX

$$$\exists S_1: \text{Solution } hζ, S_1.\text{isMinimal}$$$

Lean4

/-- If there is a solution then there is a minimal one. -/
theorem exists_minimal : ∃ (S₁ : Solution hζ), S₁.isMinimal := by
  classical
  let T := {n | ∃ (S' : Solution hζ), S'.multiplicity = n}
  rcases Nat.find_spec (⟨S.multiplicity, ⟨S, rfl⟩⟩ : T.Nonempty) with ⟨S₁, hS₁⟩
  exact ⟨S₁, fun S'' ↦ hS₁ ▸ Nat.find_min' _ ⟨S'', rfl⟩⟩

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