relIndex_inf_mul_relIndex — Mathlib

English

A relation connecting an infimum-based product of relIndex with a corresponding infimum combination.

Русский

Связь между произведением relIndex в контексте инфимума и соответствующей комбинацией инфимума.

LaTeX

$$$H.relIndex (K \\inf L) \\cdot K.relIndex L = (H \\inf K).relIndex L$$$

Lean4

@[to_additive relIndex_inf_mul_relIndex]
theorem relIndex_inf_mul_relIndex : H.relIndex (K ⊓ L) * K.relIndex L = (H ⊓ K).relIndex L := by
  rw [← inf_relIndex_right H (K ⊓ L), ← inf_relIndex_right K L, ← inf_relIndex_right (H ⊓ K) L, inf_assoc,
    relIndex_mul_relIndex (H ⊓ (K ⊓ L)) (K ⊓ L) L inf_le_right inf_le_right]

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