quotientMapOfLE — Mathlib

English

There is a map from α quotients by s to quotients by t whenever s ≤ t, given by taking representatives and projecting mod t.

Русский

Существует отображение из факторгруппы по s в факторгруппу по t при условии s ≤ t, заданное отображением по представителям в факторгруппу по t.

LaTeX

$$$\\text{If } s \\le t, \\quad \\alpha/ s \\to \\alpha/ t.$$$

Lean4

/-- If `s ≤ t`, then there is a map `α ⧸ s → α ⧸ t`. -/
@[to_additive /-- If `s ≤ t`, then there is a map `α ⧸ s → α ⧸ t`. -/
    ]
def quotientMapOfLE (h : s ≤ t) : α ⧸ s → α ⧸ t :=
  Quotient.map' id fun a b => by
    simp_rw [leftRel_eq]
    apply h

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