Theorems · Theorem · general topology

SemicontinuousAt.semicontinuousWithinAt

∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {x : α} (s : Set α),
  SemicontinuousAt r x → SemicontinuousWithinAt r s x

Defined in

Mathlib.Topology.Semicontinuity.Defs

Cited by

9 results in Mathlib

Foundations

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

Assumes

TopologicalSpace