relIndex_inf_ne_zero — Mathlib

English

If H.relIndex K = 0, then H.index = 0.

Русский

Если H.relIndex K = 0, то H.index = 0.

LaTeX

$$$H.\relIndex K = 0 \Rightarrow H.index = 0$$$

Lean4

@[to_additive]
theorem relIndex_inf_ne_zero (hH : H.relIndex L ≠ 0) (hK : K.relIndex L ≠ 0) : (H ⊓ K).relIndex L ≠ 0 :=
  by
  replace hH : H.relIndex (K ⊓ L) ≠ 0 := mt (relIndex_eq_zero_of_le_right inf_le_right) hH
  rw [← inf_relIndex_right] at hH hK ⊢
  rw [inf_assoc]
  exact relIndex_ne_zero_trans hH hK

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