Statement file: indIcc (Ingredients). This file contains exactly one declaration of the formalization's public statement surface.

noncomputable def AVenhance.indIcc (u v t : ℝ) : ℝ

Indicator (as a real function) of the closed interval [u, v].

Equations

• AVenhance.indIcc u v t = (Set.Icc u v).indicator (fun (x : ℝ) => 1) t