subgroupOf_inj — Mathlib

English

H.subgroupOf K = ⊥ iff Disjoint H K.

Русский

H.subgroupOf K = ⊥ тогда и только если H и K взаимно непересекаются.

LaTeX

$$$ H.\\mathrm{subgroupOf} K = \\perp \\iff \\mathrm{Disjoint}(H, K) $$$

Lean4

@[to_additive (attr := simp)]
theorem subgroupOf_inj {H₁ H₂ K : Subgroup G} : H₁.subgroupOf K = H₂.subgroupOf K ↔ H₁ ⊓ K = H₂ ⊓ K := by
  simpa only [SetLike.ext_iff, mem_inf, mem_subgroupOf, and_congr_left_iff] using Subtype.forall

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