Given some proposition in Lean 4, how do we state a theorem saying that we want that property to hold a number of times?

Question

I have a definition of the form in Lean 4:

def has_unbounded_limit_right (f: ℝ -> ℝ) (c : ℝ) : Prop :=
  ∀ M : ℝ, 0 < M → ∃ δ, 0 < δ ∧ ∀ x : ℝ, 0 < x - c ∧ x - c < δ → M < f x

How do I make a definition that states I want this property to hold for precisely one c, given a fixed f? My attempt is:

def count_obj_has_prop_n_times (p : Prop) (f : \R -> \R) (n : \N) : Prop := (p f) = 1
theorem one_vertical_asymptote : count_obj_has_prop_n_times has_unbounded_limit_right f 1 := by SOME_AWESOME_TACTIC_PROOF

How does one formulate statements of this sort?

For reference my current attempt for the reciprocal:

import Mathlib.Data.Real.Basic

-- define 1/x (reciprical) for reals
noncomputable def f (x : ℝ ):  ℝ := x⁻¹
#check f

-- unit test that f 1 = 1, f 2 = 1/2
theorem test_f1 : f 1 = 1 := by simp[f]
theorem test_f2 : f 2 = 2⁻¹ := by simp[f]
#print test_f1
#print test_f2

-- set_option pp.notation false
-- The limit of f x as x approaches c+ from the right is +infinity i.e., limit is unbounded from the right
-- i.e., lim_{x -> c+} f(x) = +infinity
def has_unbounded_limit_right (f: ℝ -> ℝ) (c : ℝ) : Prop :=
  ∀ M : ℝ, 0 < M → ∃ δ, 0 < δ ∧ ∀ x : ℝ, 0 < x - c ∧ x - c < δ → M < f x
#print has_unbounded_limit_right

theorem reciprocal_has_unbounded_limit_right : has_unbounded_limit_right f 0 := by
  unfold has_unbounded_limit_right
  intro M h_0_lt_M
  -- select delta that works since func is 1/x then anything less than 1/M will make f x be greater than M (so it should work)
  use M⁻¹
  -- TODO split (what did scott want with this, read)
  constructor
  . rwa [inv_pos]
  . -- consider any x with 0 < x - 0 < M⁻¹ but introduce both hypothesis 0 < x - 0 and x - 0 < M⁻¹
    intro x ⟨h_x_pos, h_x_lt_δ⟩
    -- rintro x ⟨h_x_pos, h_x_lt_δ⟩ -- TODO tomorrow, why did scott do this?
    -- rewrite both hypothesis using fact m - 0 = m
    rw [sub_zero] at h_x_pos h_x_lt_δ
    unfold f
    -- multiply both sides of h_x_lt_δ by x⁻¹ on the left using mul_lt_mul_right
    rwa [propext (lt_inv h_0_lt_M h_x_pos)]

```

Answer 1

I think it makes sense to use Cardinal here.

import Mathlib

def has_unbounded_limit_right (f: ℝ -> ℝ) (c : ℝ) : Prop :=
  ∀ M : ℝ, 0 < M → ∃ δ, 0 < δ ∧ ∀ x : ℝ, 0 < x - c ∧ x - c < δ → M < f x

noncomputable def f (x : ℝ ):  ℝ := x⁻¹

-- using `Cardinal.mk` (notation `#`)
open Cardinal
theorem one_vertical_asymptote1 : #{x : ℝ | has_unbounded_limit_right f x} = 1 := sorry

Since you just have one asymptote in your example, it also makes sense to use ExistsUnique:

-- using `ExistsUnique` (notation `∃!`)
theorem one_vertical_asymptote2 : ∃! x : ℝ, has_unbounded_limit_right f x := sorry