English
For any X, injectiveDimension X ≠ ⊤ iff there exists n with HasInjectiveDimensionLE X n.
Русский
Для любого X: injectiveDimension X не равна ⊤ тогда и только тогда существует n, такое что HasInjectiveDimensionLE X n.
LaTeX
$$\(\operatorname{injectiveDimension}(X) \neq \top \iff \exists n, \text{HasInjectiveDimensionLE}(X,n)\)$$
Lean4
theorem injectiveDimension_ne_top_iff (X : C) : injectiveDimension X ≠ ⊤ ↔ ∃ n, HasInjectiveDimensionLE X n :=
by
generalize hd : injectiveDimension X = d
induction d with
| bot =>
simp only [ne_eq, bot_ne_top, not_false_eq_true, true_iff]
exact ⟨0, by simp [← injectiveDimension_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 [← injectiveDimension_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 [← injectiveDimension_le_iff] using hd.le⟩
