Renaming

[affeldt-aist]

analysis/theories/lebesgue_integral_theory/lebesgue_integrable.v

Lines 705 to 706 in 1ab6825

	Lemma integral_fune_lt_pinfty (f : T -> \bar R) :
	mu.-integrable D f -> \int[mu]_(x in D) f x < +oo.

integrable_lty seems more appropriate