coinduced_sSup — Mathlib

English

Coinduced respects supremum over sets: coinduced f (sSup s) = sSup (image (coinduced f) s).

Русский

Коиндуцированная по f сохраняет sSup над множеством: coinduced f (sSup s) = sSup (image (coinduced f) s).

LaTeX

$$$\operatorname{coinduced} f (\mathrm{sSup} s) = \mathrm{sSup} (\mathrm{image}(\operatorname{coinduced} f) s)$$$

Lean4

@[simp]
theorem coinduced_sSup {s : Set (TopologicalSpace α)} :
    TopologicalSpace.coinduced f (sSup s) = sSup ((TopologicalSpace.coinduced f) '' s) := by
  rw [sSup_eq_iSup', sSup_image', coinduced_iSup]

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