Commit 2023-06-29 05:58 48395588

View on Github →

feat: port Archive.Imo.Imo2019Q2 (#5573)

Estimated changes

Modified Archive.lean

Created Archive/Imo/Imo2019Q2.lean

added theorem Imo2019Q2.Imo2019q2Cfg.A_mem_circumsphere

added theorem Imo2019Q2.Imo2019q2Cfg.A_ne_A₁

added theorem Imo2019Q2.Imo2019q2Cfg.A_ne_B

added theorem Imo2019Q2.Imo2019q2Cfg.A_ne_C

added theorem Imo2019Q2.Imo2019q2Cfg.A₁_ne_B

added theorem Imo2019Q2.Imo2019q2Cfg.A₁_ne_C

added def Imo2019Q2.Imo2019q2Cfg.A₂

added theorem Imo2019Q2.Imo2019q2Cfg.A₂_mem_circumsphere

added theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_A

added theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_B

added theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_C

added theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_P

added theorem Imo2019Q2.Imo2019q2Cfg.B_mem_circumsphere

added theorem Imo2019Q2.Imo2019q2Cfg.B_ne_C

added theorem Imo2019Q2.Imo2019q2Cfg.B₁_ne_C

added def Imo2019Q2.Imo2019q2Cfg.B₂

added theorem Imo2019Q2.Imo2019q2Cfg.B₂_mem_circumsphere

added theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_A₂

added theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_B

added theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_Q

added theorem Imo2019Q2.Imo2019q2Cfg.C_mem_circumsphere

added theorem Imo2019Q2.Imo2019q2Cfg.P_mem_ω

added theorem Imo2019Q2.Imo2019q2Cfg.P₁_mem_ω

added theorem Imo2019Q2.Imo2019q2Cfg.QP_parallel_BA

added theorem Imo2019Q2.Imo2019q2Cfg.Q_mem_ω

added theorem Imo2019Q2.Imo2019q2Cfg.Q_ne_B

added theorem Imo2019Q2.Imo2019q2Cfg.Q_not_mem_CB

added theorem Imo2019Q2.Imo2019q2Cfg.Q₁_mem_ω

added theorem Imo2019Q2.Imo2019q2Cfg.Q₁_ne_A₂

added theorem Imo2019Q2.Imo2019q2Cfg.affineIndependent_PQB₂

added theorem Imo2019Q2.Imo2019q2Cfg.affineIndependent_QPA₂

added theorem Imo2019Q2.Imo2019q2Cfg.collinear_PAA₁A₂

added theorem Imo2019Q2.Imo2019q2Cfg.cospherical_A₁Q₁CA₂

added theorem Imo2019Q2.Imo2019q2Cfg.cospherical_QPB₂A₂

added theorem Imo2019Q2.Imo2019q2Cfg.not_collinear_ABC

added theorem Imo2019Q2.Imo2019q2Cfg.not_collinear_CA₂A₁

added theorem Imo2019Q2.Imo2019q2Cfg.not_collinear_QPA₂

added theorem Imo2019Q2.Imo2019q2Cfg.oangle_CQ₁Q_eq_oangle_CBA

added theorem Imo2019Q2.Imo2019q2Cfg.oangle_CQ₁Q_sign_eq_oangle_CBA_sign

added theorem Imo2019Q2.Imo2019q2Cfg.result

added theorem Imo2019Q2.Imo2019q2Cfg.sOppSide_CB_Q_Q₁

added theorem Imo2019Q2.Imo2019q2Cfg.sbtw_A_A₁_A₂

added theorem Imo2019Q2.Imo2019q2Cfg.sbtw_A_B₁_C

added theorem Imo2019Q2.Imo2019q2Cfg.sbtw_B_A₁_C

added theorem Imo2019Q2.Imo2019q2Cfg.sbtw_B_B₁_B₂

added def Imo2019Q2.Imo2019q2Cfg.symm

added theorem Imo2019Q2.Imo2019q2Cfg.symm_A₂

added theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleABC

added theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleABC_circumsphere

added theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleQPA₂

added theorem Imo2019Q2.Imo2019q2Cfg.symm_ω

added theorem Imo2019Q2.Imo2019q2Cfg.symm_ω_eq_trianglePQB₂_circumsphere

added def Imo2019Q2.Imo2019q2Cfg.triangleABC

added def Imo2019Q2.Imo2019q2Cfg.trianglePQB₂

added def Imo2019Q2.Imo2019q2Cfg.triangleQPA₂

added theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA

added theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CQ₁A₁

added theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂

added theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_QB₂A₂

added theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_QQ₁A₂_eq_two_zsmul_oangle_QPA₂

added theorem Imo2019Q2.Imo2019q2Cfg.wbtw_B_Q_B₂

added def Imo2019Q2.Imo2019q2Cfg.ω

added structure Imo2019Q2.Imo2019q2Cfg

added def Imo2019Q2.someOrientation

added theorem imo2019_q2