index_inf_ne_zero — Mathlib

English

If J has finite index in K, then for any L, (J ∩ L) has finite index in (K ∩ L).

Русский

Если J имеет конечный индекс в K, то для любого L индекс J ∩ L в K ∩ L также конечен.

LaTeX

$$$\text{If } J \le G,\; K \le G,\; J_{\mathrm{relIndex}}K \neq 0 \ \Rightarrow\ (J \cap L)_{\mathrm{relIndex}}(K \cap L) \neq 0\text{ for all } L.$$$

Lean4

@[to_additive]
theorem index_inf_ne_zero (hH : H.index ≠ 0) (hK : K.index ≠ 0) : (H ⊓ K).index ≠ 0 :=
  by
  rw [← relIndex_top_right] at hH hK ⊢
  exact relIndex_inf_ne_zero hH hK

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