English
If J has nonzero index in K, then for every L, (J ⊓ L).relIndex (K ⊓ L) ≠ 0.
Русский
Если J имеет ненулевой индекс в K, то для любой L индекс (J ∩ L) в (K ∩ L) ненулевой.
LaTeX
$$$\text{If } J \relIndex K \neq 0,\; (J \cap L) \relIndex (K \cap L) \neq 0.$$$
Lean4
/-- If `J` has finite index in `K`, then `J ⊓ L` has finite index in `K ⊓ L` for any `L`. -/
@[to_additive /-- If `J` has finite index in `K`, then `J ⊓ L` has finite index in `K ⊓ L` for any
`L`. -/
]
theorem relIndex_inter_ne_zero {J K : Subgroup G} (hJK : J.relIndex K ≠ 0) (L : Subgroup G) :
(J ⊓ L).relIndex (K ⊓ L) ≠ 0 :=
by
rw [← range_subtype L, inf_comm, ← map_comap_eq, inf_comm, ← map_comap_eq, ← relIndex_comap,
comap_map_eq_self_of_injective (subtype_injective L)]
exact relIndex_comap_ne_zero _ hJK
