isComplement_range_right — Mathlib

English

Symmetric to left-range: if there exists a map with Quot.mk'' such that q = Quot.mk'' (f q) holds, then range(f) is a complement of H.

Русский

Аналогично слева: если существует отображение f с Quot.mk''(f q) = q, то range(f) является дополнением к H.

LaTeX

$$$IsComplement H (range f) \\; \\text{given } f: G \\to G\\text{ with appropriate property}$$$

Lean4

@[to_additive]
theorem isComplement_range_right {f : Quotient (QuotientGroup.rightRel H) → G} (hf : ∀ q, Quotient.mk'' (f q) = q) :
    IsComplement H (range f) := by
  rw [isComplement_subgroup_left_iff_bijective]
  refine ⟨?_, fun q ↦ ⟨⟨f q, q, rfl⟩, hf q⟩⟩
  rintro ⟨-, q₁, rfl⟩ ⟨-, q₂, rfl⟩ h
  exact Subtype.ext <| congr_arg f <| ((hf q₁).symm.trans h).trans (hf q₂)

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