relIndex_inf_le — Mathlib

English

If H.relIndex L ≠ 0 and K.relIndex L ≠ 0, then (H ⊓ K).relIndex L ≠ 0.

Русский

Если H.relIndex L ≠ 0 и K.relIndex L ≠ 0, то (H ∩ K).relIndex L ≠ 0.

LaTeX

$$(H.relIndex L ≠ 0) ∧ (K.relIndex L ≠ 0) ⇒ (H ∩ K).relIndex L ≠ 0$$

Lean4

@[to_additive]
theorem relIndex_inf_le : (H ⊓ K).relIndex L ≤ H.relIndex L * K.relIndex L :=
  by
  by_cases h : H.relIndex L = 0
  · exact (le_of_eq (relIndex_eq_zero_of_le_left inf_le_left h)).trans (zero_le _)
  rw [← inf_relIndex_right, inf_assoc, ← relIndex_mul_relIndex _ _ L inf_le_right inf_le_right, inf_relIndex_right,
    inf_relIndex_right]
  exact mul_le_mul_right' (relIndex_le_of_le_right inf_le_right h) (K.relIndex L)

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