exists_minimal_nat_zero_lt_and_lt_one

English

If f is nontrivial and bounded by 1 on naturals, there exists a minimal p with 0 < f(p) < 1 and p is minimal with that property.

Русский

Если f ненулевое и ограничено сверху единицей на натуральных, существует минимальный p, удовлетворяющий 0 < f(p) < 1, и любая другая m с тем же условием имеет p ≤ m.

LaTeX

$$∃ p:ℕ, 0

Lean4

/-- There exists a minimal positive integer with absolute value smaller than 1. -/
theorem exists_minimal_nat_zero_lt_and_lt_one : ∃ p : ℕ, (0 < f p ∧ f p < 1) ∧ ∀ m : ℕ, 0 < f m ∧ f m < 1 → p ≤ m := by
  -- There is a positive integer with absolute value different from one.

  obtain ⟨n, hn1, hn2⟩ : ∃ n : ℕ, n ≠ 0 ∧ f n ≠ 1 :=
    by
    contrapose! hf_nontriv
    refine (isNontrivial_iff_ne_trivial f).not_left.mpr <| eq_on_nat_iff_eq.mp fun n ↦ ?_
    rcases eq_or_ne n 0 with rfl | hn
    · simp
    · simp [hf_nontriv, hn]
  set P :=
    {m : ℕ | 0 < f ↑m ∧ f ↑m < 1} -- p is going to be the minimum of this set.

  have hP : P.Nonempty := ⟨n, map_pos_of_ne_zero f (Nat.cast_ne_zero.mpr hn1), lt_of_le_of_ne (bdd n) hn2⟩
  exact
    ⟨sInf P, Nat.sInf_mem hP, fun m hm ↦ Nat.sInf_le hm⟩
      -- ## Step 2: p is prime

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