Theorems · Definition · functional analysis

Set.zeroOfFactMem

{X : Type u_4} → [inst : Zero X] → (s : Set X) → [Fact (0 ∈ s)] → Zero ↑s

not marked as an instance because it would be a bad one in general, but it can be useful when working with ContinuousMapZero and the non-unital continuous functional calculus.

Defined in

Mathlib.Topology.ContinuousMap.ContinuousMapZero

Cited by

14 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

ZeroFact