mem_structured_iff_exists

formal source

 162  · intro h; subst h; exact ⟨one_pos, defect_at_one⟩
 163
 164/-- Membership in structured set ⟺ existence. -/
 165theorem mem_structured_iff_exists {x : ℝ} : x ∈ StructuredSet ↔ Exists x :=
 166  ⟨fun ⟨hpos, hdef⟩ => ⟨hpos, hdef⟩, fun ⟨hpos, hdef⟩ => ⟨hpos, hdef⟩⟩
 167
 168/-! ## Economic Inevitability -/
 169
 170/-- **Existence is Economically Inevitable**: 1 is the unique minimizer of defect. -/
 171theorem existence_economically_inevitable :
 172    ∃! x : ℝ, 0 < x ∧ ∀ y, 0 < y → defect x ≤ defect y := by
 173  refine ⟨1, ⟨one_pos, ?_⟩, ?_⟩
 174  · intro y hy
 175    rw [defect_at_one]
 176    exact defect_nonneg hy
 177  · intro z ⟨hzpos, hzmin⟩
 178    have h1 : defect z ≤ defect 1 := hzmin 1 one_pos
 179    rw [defect_at_one] at h1
 180    have h2 : defect z = 0 := le_antisymm h1 (defect_nonneg hzpos)
 181    exact (defect_zero_iff_one hzpos).mp h2
 182
 183/-! ## Complete Law of Existence -/
 184
 185/-- **Complete Law of Existence**: The following are equivalent for x > 0:
 1861. Exists x
 1872. defect(x) = 0
 1883. x ∈ StructuredSet
 1894. x = 1 -/
 190theorem complete_law_of_existence {x : ℝ} (hx : 0 < x) :
 191    Exists x ↔ defect x = 0 ∧ x ∈ StructuredSet ∧ x = 1 := by
 192  constructor
 193  · intro hex
 194    refine ⟨hex.defect_zero, mem_structured_iff_exists.mpr hex, ?_⟩
 195    exact (exists_iff_unity hx).mp hex