eq_bot_of_not_nonempty — Mathlib

English

If there is no smaller index than i (i.e., the interval Iio(i) is empty), then filtration(i) is the bottom element, i.e., filtration(i) = ⊥.

Русский

Если для индекса i не существует меньшего индекса (Iio(i) пусто), то filtration(i) является нижним элементом: filtration(i) = ⊥.

LaTeX

$$$\\text{If } Iio(i)=\\varnothing, \\quad \\mathrm{filtration}(i) = \\bot.$$$

Lean4

theorem eq_bot_of_not_nonempty (hi : ¬Nonempty (Iio i)) : filtration i = ⊥ :=
  by
  cases i
  · have := mk_ne_zero_iff.mp (rank_pos.trans_eq (mk_ord_toType <| Module.rank F E).symm).ne'
    rw [← range_coe] at hi; exact (hi inferInstance).elim
  · exact bot_unique <| adjoin_le_iff.mpr fun _ ⟨j, hj, _⟩ ↦ (hi ⟨j, coe_lt_coe.mpr hj⟩).elim

Похожие утверждения