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

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)]

$$$$

• I don't understand your question and your code for count_obj_has_prop_n_times doesn't typecheck. Surely a property either holds or it doesn't hold -- what does it mean for a property to hold n times? Commented Mar 4 at 20:56
• My guess it the OP wants to know how to state that has_unbounded_limit_right f c holds for $n$ distinct points c (and a fixed f). Commented Mar 4 at 21:52
• It probably would be good for to give a natural language explaination/example? Since your f has the same domain and codomain, are you asking about function iteration? Like unbounded_limit_right (f ∘ f ∘ f)? More generally written as has_unbounded_limit_right f^[n] 0. Commented Mar 4 at 21:54
• Oh, I think you are correct Andre. I should have read the theorem names (and not just the types). :) Commented Mar 4 at 21:56
• I assume cardinality is the standard way to handle this sort of stuff, i.e. that the cardinality of the subset unbounded_limit_right f is n. Commented Mar 4 at 22:56

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

• Curious, how did you find this? Did you googled different synonms for "number of" + Lean4 until someone came out that was useful? Or used some LLM? Commented Mar 5 at 18:11
• @CharlieParker First, this is all very standard mathematics, nothing special. Cardinality is the canonical way in math to talk about the size of a set or the number of items in a set. Also, unique existence is also a very common pattern in mathematics. To find where cardinality and unique existence were found in Mathlib, I used Moogle.ai and I happened to know that #` is a shorthand for cardinality in Lean, so then I just had to look up in the docs how to use it. As for the notation for unique existence, that is the standard notation in math so I suspected it would work in Lean. Commented Mar 5 at 22:20