IndisputableMonolith.NavierStokes.FourierExtraction

declarations in this module (19)

• theorem tendsto_comp_strictMono L19
• theorem strictMono_id_le L25
• theorem bounded_subseq_tendsto L30
• def CE L45
• def CL L54
• def LE L61
• theorem CE_zero L65
• theorem CE_succ L68
• theorem LE_strictMono L70
• theorem CE_strictMono L74
• theorem LE_conv L81
• theorem CE_conv_at L87
• theorem CE_conv_le L94
• theorem CE_factor L108
• def D L126
• theorem D_succ_gt L128
• theorem D_strictMono L136
• theorem D_converges L139
• theorem nat_diagonal_extraction L159