Commit 2025-01-23 07:01 f28d136d

View on Github →

feat(Archive/Imo): IMO 2024 Q3 (#19671) Add a formalization of IMO 2024 problem 3.

Estimated changes

Modified Archive.lean

Created Archive/Imo/Imo2024Q3.lean

added def Imo2024Q3.Condition.Big

added def Imo2024Q3.Condition.Medium

added theorem Imo2024Q3.Condition.N_add_one_lt_apply_of_apply_big_of_N'_le

added theorem Imo2024Q3.Condition.N_add_one_lt_card_filter_eq_of_small_of_N'_le

added theorem Imo2024Q3.Condition.N_add_one_lt_card_filter_eq_of_small_of_N'aux_le

added theorem Imo2024Q3.Condition.N_lt_N'

added theorem Imo2024Q3.Condition.N_lt_N'aux

added theorem Imo2024Q3.Condition.N_lt_of_apply_eq_of_apply_big_of_N'_le

added def Imo2024Q3.Condition.Small

added theorem Imo2024Q3.Condition.apply_add_one_big_of_apply_small_of_N'_le

added theorem Imo2024Q3.Condition.apply_add_one_big_of_apply_small_of_N'aux_le

added theorem Imo2024Q3.Condition.apply_add_one_eq_card

added theorem Imo2024Q3.Condition.apply_add_one_eq_card_small_le_card_eq

added theorem Imo2024Q3.Condition.apply_add_one_lt_of_apply_eq

added theorem Imo2024Q3.Condition.apply_add_one_ne_of_apply_eq

added theorem Imo2024Q3.Condition.apply_add_one_small_of_apply_big_of_N'_le

added theorem Imo2024Q3.Condition.apply_add_one_small_of_apply_big_of_N'aux_le

added theorem Imo2024Q3.Condition.apply_add_p_eq

added theorem Imo2024Q3.Condition.apply_add_two_small_of_apply_small_of_N'_le

added theorem Imo2024Q3.Condition.apply_eq_card

added theorem Imo2024Q3.Condition.apply_eq_card_small_le_card_eq_of_small

added theorem Imo2024Q3.Condition.apply_ne_zero

added theorem Imo2024Q3.Condition.apply_nth_add_one_eq

added theorem Imo2024Q3.Condition.apply_nth_add_one_eq_of_infinite

added theorem Imo2024Q3.Condition.apply_nth_add_one_eq_of_lt

added theorem Imo2024Q3.Condition.apply_sub_one_big_of_apply_small_of_N'_lt

added theorem Imo2024Q3.Condition.apply_sub_one_small_of_apply_big_of_N'_le

added theorem Imo2024Q3.Condition.apply_sub_two_small_of_apply_small_of_N'_lt

added theorem Imo2024Q3.Condition.bddAbove_setOf_infinite_setOf_apply_eq

added theorem Imo2024Q3.Condition.bddAbove_setOf_k_lt_card

added theorem Imo2024Q3.Condition.card_filter_apply_eq_Ico_add_p_le_one

added theorem Imo2024Q3.Condition.card_lt_M_of_M_le

added theorem Imo2024Q3.Condition.empty_consecutive_apply_ge_M

added theorem Imo2024Q3.Condition.even_p

added theorem Imo2024Q3.Condition.exists_a_apply_add_eq

added theorem Imo2024Q3.Condition.exists_apply_sub_two_eq_of_apply_eq

added theorem Imo2024Q3.Condition.exists_card_le_of_big

added theorem Imo2024Q3.Condition.exists_infinite_setOf_apply_eq

added theorem Imo2024Q3.Condition.exists_mem_Ico_small_and_apply_add_p_eq

added theorem Imo2024Q3.Condition.exists_p_eq

added theorem Imo2024Q3.Condition.finite_setOf_apply_eq_iff_not_small

added theorem Imo2024Q3.Condition.finite_setOf_apply_eq_k_add_one

added theorem Imo2024Q3.Condition.finite_setOf_k_lt_card

added theorem Imo2024Q3.Condition.infinite_setOf_apply_eq_anti

added theorem Imo2024Q3.Condition.infinite_setOf_apply_eq_iff_small

added theorem Imo2024Q3.Condition.infinite_setOf_apply_eq_k

added theorem Imo2024Q3.Condition.infinite_setOf_apply_eq_one

added theorem Imo2024Q3.Condition.injOn_setOf_apply_add_one_eq_of_M_le

added theorem Imo2024Q3.Condition.k_le_l

added theorem Imo2024Q3.Condition.k_lt_card_filter_eq_of_small_of_N'aux_le

added theorem Imo2024Q3.Condition.k_lt_of_big

added theorem Imo2024Q3.Condition.k_pos

added theorem Imo2024Q3.Condition.lt_card_filter_eq_of_small_nth_lt

added theorem Imo2024Q3.Condition.lt_toFinset_card

added theorem Imo2024Q3.Condition.nonempty_pSet

added theorem Imo2024Q3.Condition.nonempty_setOf_infinite_setOf_apply_eq

added theorem Imo2024Q3.Condition.not_medium_of_N'aux_lt

added theorem Imo2024Q3.Condition.not_small_of_big

added theorem Imo2024Q3.Condition.nth_apply_add_one_eq

added theorem Imo2024Q3.Condition.nth_apply_eq_zero

added theorem Imo2024Q3.Condition.nth_ne_zero_of_M_le_of_lt

added theorem Imo2024Q3.Condition.nth_sup_N_add_one_le_N'aux_of_small

added theorem Imo2024Q3.Condition.nth_sup_k_N_add_one_le_N'aux_of_small

added theorem Imo2024Q3.Condition.nth_sup_k_le_N'aux_of_small

added theorem Imo2024Q3.Condition.one_le_apply

added def Imo2024Q3.Condition.pSet

added theorem Imo2024Q3.Condition.p_apply_le_p_apply_add_two

added theorem Imo2024Q3.Condition.p_apply_sub_two_le_p_apply

added theorem Imo2024Q3.Condition.p_le_two_mul_k

added theorem Imo2024Q3.Condition.p_pos

added theorem Imo2024Q3.Condition.pos_of_big

added theorem Imo2024Q3.Condition.setOf_apply_eq_of_apply_big_of_N'_le

added theorem Imo2024Q3.Condition.small_apply_N'

added theorem Imo2024Q3.Condition.small_apply_N'_add_iff_even

added theorem Imo2024Q3.Condition.small_apply_add_two_mul_iff_small

added theorem Imo2024Q3.Condition.small_apply_sub_one_of_apply_eq_of_apply_big_of_N'_le

added theorem Imo2024Q3.Condition.small_one

added theorem Imo2024Q3.Condition.small_or_big_of_N'_le

added theorem Imo2024Q3.Condition.small_or_big_of_N'aux_lt

added def Imo2024Q3.Condition

added def Imo2024Q3.EventuallyPeriodic

added def Imo2024Q3.M

added theorem Imo2024Q3.M_pos

added theorem Imo2024Q3.N_lt_of_M_le_apply

added theorem Imo2024Q3.apply_lt_M_of_le_N

added theorem Imo2024Q3.apply_lt_of_M_le_apply

added theorem Imo2024Q3.apply_ne_of_M_le_apply

added theorem Imo2024Q3.apply_nth_zero

added theorem Imo2024Q3.map_add_one_range

added theorem Imo2024Q3.ne_zero_of_M_le_apply

added theorem Imo2024Q3.one_le_M

added theorem Imo2024Q3.result

added theorem Imo2024Q3.toFinset_card_pos