range_eq_bot_iff — Mathlib

English

For monoid hom f: G →* G', the range is trivial iff f is the trivial map.

Русский

Для гомоморфизма f: G →* G' образ тривиален тогда и только тогда, когда f тривиально.

LaTeX

$$$\operatorname{range}(f) = \bot \iff f = 1$$$

Lean4

@[to_additive]
theorem range_eq_bot_iff {f : G →* G'} : f.range = ⊥ ↔ f = 1 := by
  rw [← le_bot_iff, f.range_eq_map, map_le_iff_le_comap, top_le_iff, comap_bot, ker_eq_top_iff]

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