EnumΘ'Arg Max eq iff
enumΘ'ArgMax_eq_iff
Plain-language statement
Among the first enumerated phases, enumΘ'ArgMax returns the smallest index at which the function attains its maximum at . Equivalently, every index has value at most the value at , and every earlier index has strictly smaller value.
Source project: Carleson formalization
Person-level attribution pending.