OAI/Analysis/CircleDomains/Probability/SupportedProbabilityGDelta.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Laws supported on a G-delta form a G-delta in the weak topology. Closed-set evaluation is upper semicontinuous by portmanteau.

  1. lemma OAI.CircleDomainRigidity.isGDelta_probability_null_closed line 14
  2. lemma OAI.CircleDomainRigidity.isGDelta_supported_probabilities line 40