coinduced_le_iff_le_induced — Mathlib

English

For a map f, tα.coinduced f ≤ tβ if and only if tα ≤ tβ.induced f.

Русский

Для отображения f: tα.coinduced f ≤ tβ тогда и только тогда, когда tα ≤ tβ.induced f.

LaTeX

$$$tα.coinduced f \leq tβ \iff tα \leq tβ.induced f$$$

Lean4

theorem coinduced_le_iff_le_induced {f : α → β} {tα : TopologicalSpace α} {tβ : TopologicalSpace β} :
    tα.coinduced f ≤ tβ ↔ tα ≤ tβ.induced f :=
  ⟨fun h _s ⟨_t, ht, hst⟩ => hst ▸ h _ ht, fun h s hs => h _ ⟨s, hs, rfl⟩⟩

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