Theorems · Theorem · general topology

ContinuousMap.exists_mul_le_one_eqOn_ge

∀ {X : Type u_1} [inst : TopologicalSpace X] (f : C(X, NNReal)) {c : NNReal},
  0 < c → ∃ g, (∀ (x : X), (g * f) x ≤ 1) ∧ Set.EqOn (⇑(g * f)) 1 {x | c ≤ f x}

An auxiliary lemma used in the proof of ContinuousMap.idealOfSet_ofIdeal_eq_closure which may be useful on its own.

Defined in

Mathlib.Topology.ContinuousMap.Ideals

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace