English
For any X, projectiveDimension X ≠ ⊤ iff there exists n with HasProjectiveDimensionLE X n.
Русский
Для любого X: pd(X) ≠ ⊤ тогда и только тогда, когда существует n с HasProjectiveDimensionLE X n.
LaTeX
$$$\forall X:\mathcal C, \operatorname{projectiveDimension}(X) \neq \top \iff \exists n, HasProjectiveDimensionLE(X,n)$$$
Lean4
theorem projectiveDimension_ne_top_iff (X : C) : projectiveDimension X ≠ ⊤ ↔ ∃ n, HasProjectiveDimensionLE X n :=
by
generalize hd : projectiveDimension X = d
induction d with
| bot =>
simp only [ne_eq, bot_ne_top, not_false_eq_true, true_iff]
exact ⟨0, by simp [← projectiveDimension_le_iff, hd]⟩
| coe d =>
induction d with
| top =>
by_contra!
simp only [WithBot.coe_top, ne_eq, not_true_eq_false, false_and, true_and, false_or] at this
obtain ⟨n, hn⟩ := this
rw [← projectiveDimension_le_iff, hd, WithBot.coe_top, top_le_iff] at hn
exact ENat.coe_ne_top _ ((WithBot.coe_eq_coe).1 hn)
| coe d =>
simp only [ne_eq, WithBot.coe_eq_top, ENat.coe_ne_top, not_false_eq_true, true_iff]
exact ⟨d, by simpa only [← projectiveDimension_le_iff] using hd.le⟩
