OAI/Analysis/CircleDomains/Selection/CountableConstantPieces.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Measurability of a function that is constant on countably many closed pieces and continuous on their complement.

  1. theorem OAI.CircleDomainRigidity.measurable_of_countable_constant_pieces line 12