quotientEquivProdOfLE — Mathlib

English

If H ≤ K, there is a nonconstructive equivalence G/H ≃ G/K × K/H.

Русский

Если H ≤ K, существует нестроительная эквивалентность G/H ≃ G/K × K/H.

LaTeX

$$$\text{QuotientEquivProdOfLE}(h) : \alpha/ s \simeq (\alpha/ t) \times t/ (s/ t)$$$

Lean4

/-- If `H ≤ K`, then `G/H ≃ G/K × K/H` nonconstructively.
The constructive version is `quotientEquivProdOfLE'`. -/
@[to_additive (attr := simps!) quotientEquivProdOfLE /-- If `H ≤ K`, then `G/H ≃ G/K × K/H` nonconstructively. The
    constructive version is `quotientEquivProdOfLE'`. -/
    ]
noncomputable def quotientEquivProdOfLE (h_le : s ≤ t) : α ⧸ s ≃ (α ⧸ t) × t ⧸ s.subgroupOf t :=
  quotientEquivProdOfLE' h_le Quotient.out Quotient.out_eq'

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