range_mkQ — Mathlib

English

The range of the quotient map mkQ is the top submodule, i.e., mkQ is surjective onto the whole quotient space.

Русский

Область определения mkQ равна верхнему подмодулю, то есть mkQ сюръективен на всю фактор-модульную структуру.

LaTeX

$$$$ \\operatorname{range} (p.mkQ) = \\top. $$$$

Lean4

@[simp]
theorem range_mkQ : range p.mkQ = ⊤ :=
  eq_top_iff'.2 <| by rintro ⟨x⟩; exact ⟨x, rfl⟩

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