Naming conventions

Stream: Analysis I

[Li Xuanji]

We have theorem names like the following

theorem Sequence.isCauchy_of_const (a:ℚ) : ((fun _:ℕ ↦ a):Sequence).isCauchy := by sorry
lemma Sequence.isCauchy_of_coe (a:ℕ → ℚ) :
    (a:Sequence).isCauchy ↔ ∀ ε > (0:ℚ), ∃ N, ∀ j ≥ N, ∀ k ≥ N,
    Section_4_3.dist (a j) (a k) ≤ ε := by sorry
theorem Real.LIM_of_Cauchy {q:ℕ → ℚ} (hq: ∀ M, ∀ n ≥ M, ∀ n' ≥ M, |q n - q n'| ≤ 1 / (M+1)) :
    (q:Sequence).isCauchy ∧ ∀ M, |q M - LIM q| ≤ 1 / (M+1) := by sorry
theorem Real.add_of_LIM {a b:ℕ → ℚ} (ha: (a:Sequence).isCauchy) (hb: (b:Sequence).isCauchy) :
  LIM a + LIM b = LIM (a + b) := by sorry
theorem Real.sub_of_cauchy {a b:ℕ → ℚ} (ha: (a:Sequence).isCauchy) (hb: (b:Sequence).isCauchy) :
    ((a-b:ℕ → ℚ):Sequence).isCauchy := by sorry

I'm not completely familiar with Mathlib naming conventions, and furthermore naming conventions have some inherent flexibility/ambiguity, but my understanding is that anything appearing after an _of_ should be a hypothesis. Should we use a more consistent naming scheme for these? e.g.

• const_isCauchy
• coe_isCauchy
• add_LIM
• sub_isCauchy

Arguments for more consistency: the reader needs to interact a lot with Mathlib APIs anyway, so it would be better to use Mathlib naming convention.

I will also say I don't fully understand the best way to name ↔ theorems - e.g. apparently the following name is correct, but I find hard to use - my personal instinct is to pretend it's a → theorem, but I don't know if this would run into any other problems

lemma Equiv.isCauchy_congr {a b : Sequence}
    (hab : Equiv a b) :
    IsCauchy a ↔ IsCauchy b := by

[Kenny Lau]

this would be isCauchy_const

[Terence Tao]

Yeah, I didn't think too carefully about naming and there are certainly several places where it would better to align with Mathlib style. I suppose add_of_LIM could be LIM_add_distrib instead, and sub_of_cauchy maybe should be Sequence.isCauchy.sub instead? I guess one could find the closest Mathlib counterpart to these results as a naming guide.

[Aaron Liu]

btw that should be IsCauchy

[Li Xuanji]

Kenny Lau said:

this would be isCauchy_const

The naming convention page has toOneHom_injective though, where the prop is placed at the end

[Aaron Liu]

I would say Sequence.IsCauchy.const

[Aaron Liu]

So you can use dot notation

[Kenny Lau]

Li Xuanji said:

Kenny Lau said:

this would be isCauchy_const

The naming convention page has toOneHom_injective though, where the prop is placed at the end

injective is special case

[Li Xuanji]

Is this the guideline (from the lean4 naming doc) that recommends isCauchy_const? Since isCauchy is a function?

When encountering a function that is neither an infix notation nor a structure projection, first put the function name and then the arguments, joined by an underscore.