Antidiagonal tendsto

tendsto_sup'_antidiagonal_cofinite: If a function f : M × M → R on a Finset M, that has the antidiagonal propertry, tends to to a filter F under the cofinite filter then so does the function assigning to x : M its supremum of its antidiagonal.

theorem Finset.HasAntidiagonal.tendsto_sup'_antidiagonal_cofinite {M : Type u_1} {R : Type u_2} [AddMonoid M] [HasAntidiagonal M] {f : M × M → R} [LinearOrder R] {F : Filter R} (hf : Filter.Tendsto f Filter.cofinite F) : Filter.Tendsto (fun (a : M) => (antidiagonal a).sup' ⋯ f) Filter.cofinite F