Theorems · Theorem · general topology

BoundedContinuousFunction.extend.congr_simp

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] {δ : Type u_2}
  [inst_2 : TopologicalSpace δ] [inst_3 : DiscreteTopology δ] (f f_1 : α ↪ δ),
  f = f_1 →
    ∀ (g g_1 : BoundedContinuousFunction α β),
      g = g_1 →
        ∀ (h h_1 : BoundedContinuousFunction δ β),
          h = h_1 → BoundedContinuousFunction.extend f g h = BoundedContinuousFunction.extend f_1 g_1 h_1

Defined in

Mathlib.Topology.ContinuousMap.Bounded.Basic

Cited by

0 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpacePseudoMetricSpaceTopologicalSpaceDiscreteTopology