coinduced_continuous — Mathlib

English

The map f: α → β is continuous from α with its given topology to β equipped with the coinduced topology along f; in other words, f is continuous with respect to the coinduced topology.

Русский

Отображение f: α → β непрерывно из α с заданной топологией в β, снабжённое коиндукционной топологией по f; то есть f непрерывно относительно коиндуктивной топологии.

LaTeX

$$$\\text{Continuous}_{t, (coinduced\_f t).toTopologicalSpace}(f)$$$

Lean4

@[to_additive]
theorem coinduced_continuous {α β : Type*} [t : TopologicalSpace α] [Group β] (f : α → β) :
    Continuous[t, (coinduced f).toTopologicalSpace] f :=
  by
  rw [continuous_sInf_rng]
  rintro _ ⟨t', ht', rfl⟩
  exact continuous_iff_coinduced_le.2 ht'

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