A predicative approach to the constructive integration theory of locally compact metric spaces

Fabian Lukas Grubmüller, Iosif Petrakis

Code by ChatGPT, partly.

def chi {α : Type u_1} (A B : Set α) [DecidablePred fun (x : ↑(A ∪ B)) => ↑x ∈ A] : ↑(A ∪ B) → Bool

Equations

• chi A B x = if ↑x ∈ A then true else false