range_toContinuousMap — Mathlib

English

The range of the map toContinuousMap is exactly the set of functions f: A→B that preserve multiplication and send 1 to 1.

Русский

Образ отображения toContinuousMap равен множеству функций f: A→B, удовлетворяющим условиям сохранения умножения и единицы.

LaTeX

$$$\mathrm{range}(\mathrm{toContinuousMap}) = \{ f \in C(A,B) : f(1)=1 \land \forall x,y, f(xy)=f(x)f(y) \}$$$

Lean4

@[to_additive]
theorem range_toContinuousMap :
    Set.range (toContinuousMap : ContinuousMonoidHom A B → C(A, B)) =
      {f : C(A, B) | f 1 = 1 ∧ ∀ x y, f (x * y) = f x * f y} :=
  by
  refine Set.Subset.antisymm (Set.range_subset_iff.2 fun f ↦ ⟨map_one f, map_mul f⟩) ?_
  rintro f ⟨h1, hmul⟩
  exact ⟨{ f with map_one' := h1, map_mul' := hmul }, rfl⟩

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