Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1185 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (426 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (11 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (87 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (9 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (159 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (153 entries)
Moduleid Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (102 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (188 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (50 entries)

Global Index

A

AbstractProjectivePlane [moduleid, in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane' [moduleid, in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.a1_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.a2_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.a3 [axiom, in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.Incid [axiom, in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.incid_dec [axiom, in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.Line [axiom, in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.Point [axiom, in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.uniqueness [axiom, in ProjectiveGeometry.Plane.projective_plane_inst]
almost_pappus [lemma, in ProjectiveGeometry.Plane.P05_almost_pappus]
angle_line [lemma, in ProjectiveGeometry.Plane.P06_angle_line]
a_chasles_th [lemma, in ProjectiveGeometry.Plane.P11_chasles]


B

back [moduleid, in ProjectiveGeometry.Plane.back]
back [library]
back.a1_exist [definition, in ProjectiveGeometry.Plane.back]
back.a2_exist [definition, in ProjectiveGeometry.Plane.back]
back.a3 [definition, in ProjectiveGeometry.Plane.back]
back.case1 [lemma, in ProjectiveGeometry.Plane.back]
back.case2 [lemma, in ProjectiveGeometry.Plane.back]
back.case3 [lemma, in ProjectiveGeometry.Plane.back]
back.case4 [lemma, in ProjectiveGeometry.Plane.back]
back.Incid [definition, in ProjectiveGeometry.Plane.back]
back.incid_dec [definition, in ProjectiveGeometry.Plane.back]
back.Line [definition, in ProjectiveGeometry.Plane.back]
back.Point [definition, in ProjectiveGeometry.Plane.back]
back.uniq [moduleid, in ProjectiveGeometry.Plane.back]
back.uniqueness [definition, in ProjectiveGeometry.Plane.back]
basic_facts [library]
basic_facts_plane [library]
bij [definition, in ProjectiveGeometry.Plane.bij]
bij [library]
BuildFSets [moduleid, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.couple [definition, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.couple_singleton_eq [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.couple_1 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.Dec [moduleid, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.FiniteSetsOfPoints [moduleid, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.FiniteSetsOfPointsProperties [moduleid, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.FM [moduleid, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.inter_fsetdecide_1 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.inter_fsetdecide_2 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.inter_fsetdecide_4 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.inter_fsetdecide_5 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.Point [definition, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.quadruple [definition, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.set_of_points [definition, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.subset_exists [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.test [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.test2 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.test_fsetdec [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.test_fsetdec2 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple [definition, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_couple_1 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_couple_2 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_couple_3 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_couple_4 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_couple_5 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_couple_6 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_1 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_2 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_3 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_4 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_5 [lemma, in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.union_fsetdecide [lemma, in ProjectiveGeometry.Space.sets_of_points]


C

c [lemma, in ProjectiveGeometry.Plane.examples]
cevian_in [definition, in ProjectiveGeometry.Plane.P07_cevian_lines]
cevian_lines [lemma, in ProjectiveGeometry.Plane.P07_cevian_lines]
cevian_lines_2 [lemma, in ProjectiveGeometry.Plane.P08_cevian_lines_2]
characterization [lemma, in ProjectiveGeometry.Plane.flat]
CoherentProjectivePlane [moduleid, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.a1_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.a2_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.a3_1 [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.a3_2 [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.Incid [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.incid_dec [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.Line [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.l1 [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.l2 [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.Point [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.uniqueness [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
Col [definition, in ProjectiveGeometry.Plane.hexamys]
col_col_on_inter [lemma, in ProjectiveGeometry.Plane.hexamys]
col_comm [lemma, in ProjectiveGeometry.Plane.hexamys]
col_comm2 [lemma, in ProjectiveGeometry.Plane.hexamys]
col_comm3 [lemma, in ProjectiveGeometry.Plane.hexamys]
col_comm4 [lemma, in ProjectiveGeometry.Plane.hexamys]
col_comm5 [lemma, in ProjectiveGeometry.Plane.hexamys]
col_incid [lemma, in ProjectiveGeometry.Plane.hexamys]
col_line_eq [lemma, in ProjectiveGeometry.Plane.hexamys]
Col_on [definition, in ProjectiveGeometry.Plane.hexamys]
col_trivial_1 [lemma, in ProjectiveGeometry.Plane.hexamys]
col_trivial_2 [lemma, in ProjectiveGeometry.Plane.hexamys]
col_trivial_3 [lemma, in ProjectiveGeometry.Plane.hexamys]
complete_quadrilateral [lemma, in ProjectiveGeometry.Plane.P09_complete_quadrilateral]
complete_quadrilateral_2 [lemma, in ProjectiveGeometry.Plane.P10_complete_quadrilateral_2]
CoxeterProjectivePlane [moduleid, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.a1_unique [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.a2_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.a2_17 [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.a3 [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.bijective [definition, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.collinear [definition, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.Incid [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.incid_dec [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.injective [definition, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.is_elementary_projectivity [definition, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.is_inter [definition, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.is_perspectivity [definition, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.Line [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.l2_18 [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.Point [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.surjective [definition, in ProjectiveGeometry.Plane.projective_plane_axioms]


D

decid [moduleid, in ProjectiveGeometry.Plane.flat]
decid [moduleid, in ProjectiveGeometry.Plane.bij]
decidability [moduleid, in ProjectiveGeometry.Plane.decidability]
Decidability [moduleid, in ProjectiveGeometry.Plane.decidability]
decidability [library]
decidability.eq_line_dec [lemma, in ProjectiveGeometry.Plane.decidability]
Decidability.eq_line_dec [axiom, in ProjectiveGeometry.Plane.decidability]
decidability.eq_point_dec [lemma, in ProjectiveGeometry.Plane.decidability]
Decidability.eq_point_dec [axiom, in ProjectiveGeometry.Plane.decidability]
decidability.eq_point_dec_sublemma [lemma, in ProjectiveGeometry.Plane.decidability]
decidability.first_point [lemma, in ProjectiveGeometry.Plane.decidability]
Decidability.Incid [axiom, in ProjectiveGeometry.Plane.decidability]
decidability.Incid [definition, in ProjectiveGeometry.Plane.decidability]
decidability.incid_dec2 [lemma, in ProjectiveGeometry.Plane.decidability]
decidability.Line [definition, in ProjectiveGeometry.Plane.decidability]
Decidability.Line [axiom, in ProjectiveGeometry.Plane.decidability]
decidability.outsider [lemma, in ProjectiveGeometry.Plane.decidability]
Decidability.outsider [axiom, in ProjectiveGeometry.Plane.decidability]
decidability.Point [definition, in ProjectiveGeometry.Plane.decidability]
Decidability.Point [axiom, in ProjectiveGeometry.Plane.decidability]
decidability.ProjectivePlane' [moduleid, in ProjectiveGeometry.Plane.decidability]
decidability.second_line [lemma, in ProjectiveGeometry.Plane.decidability]
decidability.second_point [lemma, in ProjectiveGeometry.Plane.decidability]
decidability.third_point [lemma, in ProjectiveGeometry.Plane.decidability]
decidability.uniq [moduleid, in ProjectiveGeometry.Plane.decidability]
Desargues [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
DesarguesxD [moduleid, in ProjectiveGeometry.Space.desarguesxD]
desarguesxD [library]
DesarguesxD.desargues_theorem [section, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.A [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.alpha [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.A' [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.B [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.beta [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.B' [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.C [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.C' [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.gamma [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.O [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rAA' [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rAA'O [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rABC [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rABgamma [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rABO [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rACbeta [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rACO [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rA'B'C' [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rA'B'gamma [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rA'C'beta [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rBB' [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rBB'O [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rBCalpha [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rBCO [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rB'C'alpha [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rCC' [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rCC'O [variable, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.Desargues_xD [lemma, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.Desargues_xD' [lemma, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.Desargues_2D [moduleid, in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.Desargues_3D [moduleid, in ProjectiveGeometry.Space.desarguesxD]
Desargues.Desargues [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.M2 [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_B [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_B' [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_C [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_C' [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_D [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_D' [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_E [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_E' [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_F [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_F' [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_G [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_G' [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
desargues2D [library]
Desargues2Dfinal [moduleid, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.Desargues_plane [lemma, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem [section, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.A [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.alpha [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.A' [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.B [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.beta [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.B' [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.C [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.C' [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.gamma [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.O [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rAA' [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rAA'O [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rABC [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rABCA'B'C'O [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rABgamma [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rABO [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rACbeta [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rACO [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rA'B'C' [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rA'B'gamma [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rA'C'beta [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rA'O [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rBB' [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rBB'O [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rBCalpha [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rBCO [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rB'C'alpha [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rB'O [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rCC' [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rCC'O [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rC'O [variable, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.Desargues_2D_lem3 [moduleid, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.Desargues_3D [moduleid, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.rA'B'O' [lemma, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.rA'C'O' [lemma, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.rB'C'O' [lemma, in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal2 [moduleid, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.Desargues_plane [lemma, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem [section, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.A [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.alpha [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.A' [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.B [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.beta [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.B' [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.C [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.C' [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.gamma [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.O [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rAA' [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rAA'O [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rABC [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rABCA'B'C'O [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rABgamma [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rABO [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rACbeta [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rACO [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rA'B'C' [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rA'B'gamma [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rA'C'beta [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rBB' [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rBB'O [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rBCalpha [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rBCO [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rB'C'alpha [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rCC' [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rCC'O [variable, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.Desargues_2D_final [moduleid, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.new_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dlemmas [moduleid, in ProjectiveGeometry.Space.desargues2Dlemmas]
desargues2Dlemmas [library]
Desargues2Dlemmas.l1_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.l2rABMP_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.Props [moduleid, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rABCc_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rABCO [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rABOc_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rABOo_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rCC'oc_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rCC'oPc_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rcC'_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rcC_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rco_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rPcC'oO_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rPC'oc_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.subl2rABMP_scheme [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas2 [moduleid, in ProjectiveGeometry.Space.desargues2Dlemmas2]
desargues2Dlemmas2 [library]
Desargues2Dlemmas2.desargues_plane [section, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.A [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.A' [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.B [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.B' [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.C [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.C' [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.O [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists [section, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists [section, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.a_exists [section, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.a_exists.a [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.a_exists.rka2 [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.a_exists.rka2' [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.b_exists [section, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.b_exists.b [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.b_exists.rkb2 [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.b_exists.rkb2' [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.c_exists [section, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.c_exists.c [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.c_exists.rkc2 [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.c_exists.rkc2' [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.o [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.rko1 [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.rko2 [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.rko3 [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.P [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.rABOP [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.rOP [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rAA' [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rAA'O [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rABC [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rABCA'B'C'O [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rABO [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rACO [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rA'B'C' [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rA'B'O' [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rA'C'O' [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rBB' [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rBB'O [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rBCO [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rB'C'O' [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rCC' [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rCC'O [variable, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.Desargues_plane_lem [moduleid, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.ex_o [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l1A'B'O [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l1A'C'O [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l1B'C'O [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l2rABMP [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l2rABOP [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l2rACMP [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l2rA'B'OP [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.perm3 [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.ra [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rABCa [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rABCc [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rABCo [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rABOb [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rABOc [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rABOo [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rACMo [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rACOo [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rACOP [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rAO [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rao [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rA'B'Mo [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rA'B'Oo [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rA'C'Mo [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rA'C'Oo [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rA'C'OP [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rA'O [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rb [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rBCOP [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rbo [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rBO [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rB'C'OP [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rB'O [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rc [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rcC [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rcC' [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rCC'oc [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rCC'oPc [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rco [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rCO [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rC'O [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas3 [moduleid, in ProjectiveGeometry.Space.desargues2Dlemmas3]
desargues2Dlemmas3 [library]
Desargues2Dlemmas3.beta_ok' [lemma, in ProjectiveGeometry.Space.desargues2Dlemmas3]
Desargues2Dlemmas3.Desargues_plane_lem [moduleid, in ProjectiveGeometry.Space.desargues2Dlemmas3]
Desargues2Dlemmas3.Desargues_plane_lem2 [moduleid, in ProjectiveGeometry.Space.desargues2Dlemmas3]
desargues2Dmore [library]
Desargues3D [moduleid, in ProjectiveGeometry.Space.desargues3D]
desargues3D [library]
Desargues3DLemmas [moduleid, in ProjectiveGeometry.Space.desargues3Dlemmas]
desargues3Dlemmas [library]
Desargues3DLemmas.A_not_beta_scheme [lemma, in ProjectiveGeometry.Space.desargues3Dlemmas]
Desargues3DLemmas.a_not_gamma_scheme [lemma, in ProjectiveGeometry.Space.desargues3Dlemmas]
Desargues3DLemmas.Props [moduleid, in ProjectiveGeometry.Space.desargues3Dlemmas]
Desargues3DLemmas.rbA_scheme [lemma, in ProjectiveGeometry.Space.desargues3Dlemmas]
Desargues3DLemmas.sublemma [lemma, in ProjectiveGeometry.Space.desargues3Dlemmas]
Desargues3DLemmas.sublemma'' [lemma, in ProjectiveGeometry.Space.desargues3Dlemmas]
Desargues3Dspecial [moduleid, in ProjectiveGeometry.Space.desargues3Dspecial]
desargues3Dspecial [library]
Desargues3Dspecial.Desargues [lemma, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues [section, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.A [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.a [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.alpha [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.B [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.b [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.beta [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.C [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.c [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.gamma [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.O [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.raAO [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rABC [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rabc [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rABCabc [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rabgamma [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rABgamma [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.racbeta [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rACbeta [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rbBO [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rbcalpha [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rBCalpha [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rcCO [variable, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues3D [moduleid, in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3D.A_not_alpha [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.a_not_alpha [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.A_not_beta [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.A_not_gamma [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.a_not_gamma [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.B_not_alpha [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.B_not_beta [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.b_not_gamma [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.B_not_gamma [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.C_not_alpha [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.C_not_beta [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.c_not_beta [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.C_not_gamma [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues3DLemmas [moduleid, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general [section, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.a [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.A [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.alpha [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.b [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.B [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.beta [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.C [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.c [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.gamma [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.O [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.raA [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.raAO [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rABC [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rabc [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rABCabc [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rABgamma [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rabgamma [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rACbeta [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.racbeta [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rbB [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rbBO [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rbcalpha [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rBCalpha [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rcC [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rcCO [variable, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L1alpha [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L1palpha [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L1Pbeta [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L1pbeta [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L1pgamma [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L1Pgamma [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L2p [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L2P [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Ps [definition, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.ps [definition, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rAB [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rab [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rac [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rAC [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.ralphabeta [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.ralphagamma [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rbc [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rBC [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rbetagamma [lemma, in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rPpalbega [lemma, in ProjectiveGeometry.Space.desargues3D]
desargues_cevian_case [lemma, in ProjectiveGeometry.Plane.hexamys_desargues]
Desargues_from_A [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.collinear [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.collinearPPQ [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.collinearPQP [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.collinearPQQ [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_degen_1 [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_degen_2 [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_degen_3 [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_1 [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_2 [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_3 [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_4 [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_5 [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.Desargues_from_A [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.Desargues_from_A_spec [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.not_all_equal [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.on_line [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
dist3 [definition, in ProjectiveGeometry.Plane.general_tactics]
dist3 [definition, in ProjectiveGeometry.Space.general_tactics]
dist4 [definition, in ProjectiveGeometry.Plane.general_tactics]
dist4 [definition, in ProjectiveGeometry.Space.general_tactics]
dist6 [definition, in ProjectiveGeometry.Plane.general_tactics]
dist_3 [definition, in ProjectiveGeometry.Space.projective_space_axioms]
dist_4 [definition, in ProjectiveGeometry.Space.projective_space_axioms]


E

eolien [lemma, in ProjectiveGeometry.Plane.P12_aeolian]
essai [lemma, in ProjectiveGeometry.Plane.hexamys]
example [moduleid, in ProjectiveGeometry.Plane.projective_plane_duality]
examples [library]
example.dual_example [lemma, in ProjectiveGeometry.Plane.projective_plane_duality]
example.Swaped [moduleid, in ProjectiveGeometry.Plane.projective_plane_duality]


F

FanoPlane [moduleid, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.A [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.ABF [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.ADG [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.a1_exist [lemma, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.a1_unique [lemma, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.a2_exist [lemma, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.a2_unique [lemma, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.a3 [lemma, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.B [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.BCD [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.BEG [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.C [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.CAE [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.CFG [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.D [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.DEF [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.degen_line [lemma, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.degen_point [lemma, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.E [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.F [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.G [constructor, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.Incid [definition, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.Incid_bool [definition, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.incid_dec [lemma, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.ind_line [inductive, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.ind_Point [inductive, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.Line [definition, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.Point [definition, in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.uniqueness [lemma, in ProjectiveGeometry.Plane.fano_plane]
fano_plane [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane [library]
fano_plane.A [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.ABF [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.ADG [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.B [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.BCD [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.BEG [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.C [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.CAE [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.CFG [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.D [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.DEF [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.E [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.F [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.G [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.Incid [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.is_fano_plane [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.is_fano_plane_inst [axiom, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.is_only_7_lines [axiom, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.is_only_7_pts [axiom, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.Line [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.Point [variable, in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane_desargues [library]
field_variable_isolation_tactic [library]
field_variable_isolation_tactic [library]
flat [definition, in ProjectiveGeometry.Plane.flat]
flat [library]
forth [moduleid, in ProjectiveGeometry.Plane.forth]
forth [library]
forth.a1_exist [definition, in ProjectiveGeometry.Plane.forth]
forth.a2_exist [definition, in ProjectiveGeometry.Plane.forth]
forth.a3_1 [definition, in ProjectiveGeometry.Plane.forth]
forth.a3_2 [definition, in ProjectiveGeometry.Plane.forth]
forth.cas1 [lemma, in ProjectiveGeometry.Plane.forth]
forth.cas2 [lemma, in ProjectiveGeometry.Plane.forth]
forth.cas3 [lemma, in ProjectiveGeometry.Plane.forth]
forth.Incid [definition, in ProjectiveGeometry.Plane.forth]
forth.incid_dec [definition, in ProjectiveGeometry.Plane.forth]
forth.Line [definition, in ProjectiveGeometry.Plane.forth]
forth.Point [definition, in ProjectiveGeometry.Plane.forth]
forth.uniq [moduleid, in ProjectiveGeometry.Plane.forth]
forth.uniqueness [definition, in ProjectiveGeometry.Plane.forth]
fp_empty [lemma, in ProjectiveGeometry.Plane.flat]
fp_line [lemma, in ProjectiveGeometry.Plane.flat]
fp_plane [lemma, in ProjectiveGeometry.Plane.flat]
fp_singleton [lemma, in ProjectiveGeometry.Plane.flat]


G

general_tactics [library]
general_tactics [library]


H

hexamy [definition, in ProjectiveGeometry.Plane.hexamys]
hexamys [library]
hexamys_desargues [library]
hexamy_desargues_gen_case [lemma, in ProjectiveGeometry.Plane.hexamys_desargues]
hexamy_prop [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_rot_left [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_rot_right [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_special_case [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_right [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_2_3 [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_2_4 [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_2_5 [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_2_6 [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_3_4 [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_3_5 [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_3_6 [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_4_5 [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_4_6 [lemma, in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_5_6 [lemma, in ProjectiveGeometry.Plane.hexamys]
HeytingProjectivePlane [moduleid, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.Apart [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.apart_l [definition, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.Incid [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.Line [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.out [definition, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.Point [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P1 [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P2 [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P3 [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P4 [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P5i [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P5ii [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P5iii [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.S1 [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.S2 [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.S3 [axiom, in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
Heyting_projective_plane_axioms [library]
homogeneous [library]
HomogenousCoords [moduleid, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.a1_exist [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.a2_exist [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.a3_1 [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.a3_2 [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.det2 [definition, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.equiv_and [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.equiv_eq [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.equiv_or [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.eq_point_dec [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.eq_1 [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.eq_2 [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.general_line_through [definition, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.general_point_through [definition, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.Incid [definition, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.incid_dec [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.Incid_triple [definition, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.IndLine [inductive, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.IndPoint [inductive, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.inner_product_triple [definition, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.Line [definition, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.line_of_triple [definition, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.L0 [constructor, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.L1 [constructor, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.L2 [constructor, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.normalize_compat_incid [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.Point [definition, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.point_of_triple [definition, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.point_of_triple_functionnal [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.point_triple [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.P0 [constructor, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.P1 [constructor, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.P2 [constructor, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.triple_of_line [definition, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.triple_of_point [definition, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.triple_point [lemma, in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.uniqueness [lemma, in ProjectiveGeometry.Plane.homogeneous]


I

incid_inter_left [lemma, in ProjectiveGeometry.Plane.hexamys]
incid_inter_right [lemma, in ProjectiveGeometry.Plane.hexamys]
incid_line_left [lemma, in ProjectiveGeometry.Plane.hexamys]
incid_line_right [lemma, in ProjectiveGeometry.Plane.hexamys]
Incid_property [lemma, in ProjectiveGeometry.Plane.examples]
included_or_not [lemma, in ProjectiveGeometry.Plane.flat]
inj [definition, in ProjectiveGeometry.Plane.bij]
inter [definition, in ProjectiveGeometry.Plane.hexamys]
inter_comm [lemma, in ProjectiveGeometry.Plane.hexamys]
is_hexamy [definition, in ProjectiveGeometry.Plane.hexamys]
is_on_inter [definition, in ProjectiveGeometry.Plane.hexamys]
is_on_proper_inter [definition, in ProjectiveGeometry.Plane.hexamys]
is_on_proper_inter_is_on_inter [lemma, in ProjectiveGeometry.Plane.hexamys]
is_transverse [definition, in ProjectiveGeometry.Plane.hexamys]


L

Lc [lemma, in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lc [lemma, in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcdiv1 [lemma, in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcdiv1 [lemma, in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcdiv2 [lemma, in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcdiv2 [lemma, in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcinv [lemma, in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcinv [lemma, in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcmult1 [lemma, in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcmult1 [lemma, in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcmult2 [lemma, in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcmult2 [lemma, in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcm1 [lemma, in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcm1 [lemma, in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcm2 [lemma, in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcm2 [lemma, in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcop1 [lemma, in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcop1 [lemma, in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcp1 [lemma, in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcp1 [lemma, in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcp2 [lemma, in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcp2 [lemma, in ProjectiveGeometry.Space.field_variable_isolation_tactic]
line [definition, in ProjectiveGeometry.Plane.hexamys]
line_as_set_of_points [definition, in ProjectiveGeometry.Plane.bij]
line_comm [lemma, in ProjectiveGeometry.Plane.hexamys]
line_neq_neq [lemma, in ProjectiveGeometry.Plane.hexamys]
line_set_of_points [lemma, in ProjectiveGeometry.Plane.bij]
line_wd [lemma, in ProjectiveGeometry.Plane.hexamys]
line_wd_sym [lemma, in ProjectiveGeometry.Plane.hexamys]


M

Matroid [moduleid, in ProjectiveGeometry.Space.matroids_axioms]
matroids_axioms [library]
matroids_properties [library]
Matroid' [moduleid, in ProjectiveGeometry.Space.matroids_axioms]
Matroid'.FiniteSetsDefs [moduleid, in ProjectiveGeometry.Space.matroids_axioms]
Matroid'.matroid1' [axiom, in ProjectiveGeometry.Space.matroids_axioms]
Matroid'.matroid2' [axiom, in ProjectiveGeometry.Space.matroids_axioms]
Matroid'.matroid3' [axiom, in ProjectiveGeometry.Space.matroids_axioms]
Matroid'.rk [axiom, in ProjectiveGeometry.Space.matroids_axioms]
Matroid'.rk_compat [axiom, in ProjectiveGeometry.Space.matroids_axioms]
Matroid.FiniteSetsDefs [moduleid, in ProjectiveGeometry.Space.matroids_axioms]
Matroid.matroid1_a [axiom, in ProjectiveGeometry.Space.matroids_axioms]
Matroid.matroid1_b [axiom, in ProjectiveGeometry.Space.matroids_axioms]
Matroid.matroid2 [axiom, in ProjectiveGeometry.Space.matroids_axioms]
Matroid.matroid3 [axiom, in ProjectiveGeometry.Space.matroids_axioms]
Matroid.rk [axiom, in ProjectiveGeometry.Space.matroids_axioms]
Matroid_Properties [moduleid, in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.add_inj [lemma, in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.cardinal_couple [lemma, in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.eq_point_dec [lemma, in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.matroid1_b_useful [lemma, in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.matroid3'_gen [lemma, in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.matroid3_useful [lemma, in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.M' [moduleid, in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.rk_couple_2 [lemma, in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.rk_quadruple_le [lemma, in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.rk_singleton_le [lemma, in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.rk_triple_le [lemma, in ProjectiveGeometry.Space.matroids_properties]
matroid_to_matroid' [moduleid, in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.add_union_singleton_sym [lemma, in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.FiniteSetsDefs [moduleid, in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.matroid1' [lemma, in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.matroid2' [lemma, in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.matroid3' [lemma, in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.matroid3_useful [lemma, in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.rk [definition, in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.rk_compat [lemma, in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.rk_singleton [lemma, in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.test_fsetdec [lemma, in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid_p [library]
Meet [definition, in ProjectiveGeometry.Plane.hexamys]
Moulton [moduleid, in ProjectiveGeometry.Plane.moulton]
moulton [library]
Moulton.a1_exist [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.a2_exist [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.a3_1 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.a3_2 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.collinear [definition, in ProjectiveGeometry.Plane.moulton]
Moulton.dir [constructor, in ProjectiveGeometry.Plane.moulton]
Moulton.equiv_and [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.equiv_eq [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.equiv_or [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.eq_point_dec [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.foo [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.hint0 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.hint1 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.hint2 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.hint2' [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.hint2'' [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.hint3 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.hint4 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.hint5 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.hint6 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.hint7 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.Incid [definition, in ProjectiveGeometry.Plane.moulton]
Moulton.incid_dec [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.IndLine [inductive, in ProjectiveGeometry.Plane.moulton]
Moulton.IndPoint [inductive, in ProjectiveGeometry.Plane.moulton]
Moulton.Infinite [constructor, in ProjectiveGeometry.Plane.moulton]
Moulton.is_equiv [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.L [constructor, in ProjectiveGeometry.Plane.moulton]
Moulton.Line [definition, in ProjectiveGeometry.Plane.moulton]
Moulton.non_collinear [definition, in ProjectiveGeometry.Plane.moulton]
Moulton.non_desarguesian [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.normalize_not [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.on_line [definition, in ProjectiveGeometry.Plane.moulton]
Moulton.P [constructor, in ProjectiveGeometry.Plane.moulton]
Moulton.Point [definition, in ProjectiveGeometry.Plane.moulton]
Moulton.R_pos_neg [axiom, in ProjectiveGeometry.Plane.moulton]
Moulton.strict_or_not [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.sub_lemma1 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.sub_lemma2 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.sub_lemma3 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.sub_lemma4 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.sys_eqs_1 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.sys_eqs_2 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.sys_eqs_3 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.sys_eqs_4 [lemma, in ProjectiveGeometry.Plane.moulton]
Moulton.uniqueness [lemma, in ProjectiveGeometry.Plane.moulton]


N

not_eq_sym_line [lemma, in ProjectiveGeometry.Plane.hexamys]
not_eq_sym_point [lemma, in ProjectiveGeometry.Plane.hexamys]


O

one_not_two [lemma, in ProjectiveGeometry.Plane.homogeneous]
one_not_two [lemma, in ProjectiveGeometry.Plane.moulton]
on_inter [definition, in ProjectiveGeometry.Plane.hexamys]
on_inter' [definition, in ProjectiveGeometry.Plane.hexamys]
on_inter_points_wd [lemma, in ProjectiveGeometry.Plane.hexamys]
on_inter_points_wd_spec_1 [lemma, in ProjectiveGeometry.Plane.hexamys]
on_inter_points_wd_spec_2 [lemma, in ProjectiveGeometry.Plane.hexamys]
on_inter_points_wd_spec_3 [lemma, in ProjectiveGeometry.Plane.hexamys]
on_inter_points_wd_spec_4 [lemma, in ProjectiveGeometry.Plane.hexamys]
on_inter_wd [lemma, in ProjectiveGeometry.Plane.hexamys]
on_inter_wd_sym [lemma, in ProjectiveGeometry.Plane.hexamys]


P

pappus_pappus_strong [lemma, in ProjectiveGeometry.Plane.hexamys]
pappus_strong [definition, in ProjectiveGeometry.Plane.hexamys]
pappus_weak [definition, in ProjectiveGeometry.Plane.hexamys]
pempty [definition, in ProjectiveGeometry.Plane.flat]
PG25 [moduleid, in ProjectiveGeometry.Plane.pg25]
pg25 [library]
PG25.a1_exist [lemma, in ProjectiveGeometry.Plane.pg25]
PG25.a2_exist [lemma, in ProjectiveGeometry.Plane.pg25]
PG25.a3 [lemma, in ProjectiveGeometry.Plane.pg25]
PG25.Incid [definition, in ProjectiveGeometry.Plane.pg25]
PG25.Incid_bool [definition, in ProjectiveGeometry.Plane.pg25]
PG25.incid_dec [lemma, in ProjectiveGeometry.Plane.pg25]
PG25.ind_line [inductive, in ProjectiveGeometry.Plane.pg25]
PG25.ind_point [inductive, in ProjectiveGeometry.Plane.pg25]
PG25.Line [definition, in ProjectiveGeometry.Plane.pg25]
PG25.l0 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l1 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l10 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l11 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l12 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l13 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l14 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l15 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l16 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l17 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l18 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l19 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l2 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l20 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l21 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l22 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l23 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l24 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l25 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l26 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l27 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l28 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l29 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l3 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l30 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l4 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l5 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l6 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l7 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l8 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.l9 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.Point [definition, in ProjectiveGeometry.Plane.pg25]
PG25.P0 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P1 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P10 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P11 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P12 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P13 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P14 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P15 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P16 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P17 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P18 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P19 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P2 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P20 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P21 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P22 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P23 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P24 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P25 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P26 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P27 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P28 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P29 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P3 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P30 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P4 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P5 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P6 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P7 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P8 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.P9 [constructor, in ProjectiveGeometry.Plane.pg25]
PG25.uniqueness [lemma, in ProjectiveGeometry.Plane.pg25]
pline [definition, in ProjectiveGeometry.Plane.flat]
pplane [definition, in ProjectiveGeometry.Plane.flat]
PreProjectivePlane [moduleid, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane.a1_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane.a2_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane.Incid [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane.incid_dec [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane.Line [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane.Point [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane.uniqueness [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2 [moduleid, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.a1_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.a1_unique [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.a2_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.a2_unique [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.Incid [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.incidABl [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.incidAl1l2 [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.incid_dec [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.Line [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.Point [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.uniqueness [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane [moduleid, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane' [moduleid, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.a1_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.a2_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.a3_1 [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.a3_2 [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.Incid [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.incid_dec [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.Line [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.Point [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.uniqueness [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.a1_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.a2_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.a3 [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.Incid [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.incid_dec [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.Line [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.Point [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.uniqueness [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2 [moduleid, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2HeytingProjectivePlane [moduleid, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.Apart [definition, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.apart_l [definition, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.Facts [moduleid, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.Incid [definition, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.Line [definition, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.M' [moduleid, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.out [definition, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.Point [definition, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.P1 [lemma, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.P2 [lemma, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.P3 [lemma, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.P4 [lemma, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.P5i [lemma, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.P5ii [lemma, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.P5iii [lemma, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.S1 [lemma, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.S2 [lemma, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.S3 [lemma, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.uniq [moduleid, in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2.a1_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.a1_unique [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.a2_exist [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.a2_unique [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.a3_1 [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.a3_2 [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.Incid [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.incid_dec [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.Line [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.Point [axiom, in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectiveSpace [moduleid, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceFacts [moduleid, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.a1_unique [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.a2_unique [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.a3_3simplified [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.eq_line_dec [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.Incid [definition, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.incidABl [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.incidAl1l2 [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.Incid_mor [axiom, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.Line [definition, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.only_one_intersection [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.Point [definition, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.second_line [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.second_point [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.third_line [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.third_point [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.two_lines_aux [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.two_lines_P [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.two_points_not_incident_l1l2 [lemma, in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceOrHigher [moduleid, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.a1_exists [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.a2 [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.a3_1 [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.a3_2 [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.dist3 [definition, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.dist4 [definition, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.Incid [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.incid_dec [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.Line [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.line_eq [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.line_eq_refl [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.line_eq_sym [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.line_eq_trans [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.Point [definition, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.uniqueness [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.a1_exists [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.a2 [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.a3_1 [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.a3_2 [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.a3_3 [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.dist3 [definition, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.dist4 [definition, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.Incid [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.incid_dec [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.Intersect [definition, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.Intersect_In [definition, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.Line [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.Point [definition, in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.uniqueness [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
projective_plane_axioms [library]
projective_plane_duality [library]
projective_plane_inst [library]
projective_plane_to_Heyting_projective_plane [library]
projective_space_axioms [library]
projective_space_rank_axioms [library]
projective_space_rank_to_projective_space [library]
proof_irr [axiom, in ProjectiveGeometry.Plane.bij]
pset [definition, in ProjectiveGeometry.Plane.flat]
pset_decompose [lemma, in ProjectiveGeometry.Plane.flat]
pseudo_midpoint [lemma, in ProjectiveGeometry.Plane.P14_pseudo_midpoint]
psingleton [definition, in ProjectiveGeometry.Plane.flat]
P05_almost_pappus [library]
P06_angle_line [library]
P07_cevian_lines [library]
P08_cevian_lines_2 [library]
P09_complete_quadrilateral [library]
P10_complete_quadrilateral_2 [library]
P11_chasles [library]
P12_aeolian [library]
P14_pseudo_midpoint [library]


R

RankProjectiveSpace [moduleid, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpaceToProjectiveSpaceOrHigher [moduleid, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.a1_exists [lemma, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.a2 [lemma, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.a3_1 [lemma, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.a3_2 [lemma, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.Cline [constructor, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.dist3 [definition, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.dist4 [definition, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.fstP [definition, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.Incid [definition, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.incid_dec [lemma, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.Line [definition, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.LineInd [inductive, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.line_eq [definition, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.line_eq_refl [lemma, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.line_eq_sym [lemma, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.line_eq_trans [lemma, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.Point [definition, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.Props [moduleid, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.second_point [lemma, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.sndP [definition, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.uniqueness [lemma, in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpace.FiniteSetsDefs [moduleid, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.lower_dim [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.matroid1_a [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.matroid1_b [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.matroid2 [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.matroid3 [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.pasch [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.Point [definition, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.P0 [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.P1 [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.P2 [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.P3 [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.rk [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.rk_couple_ge [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.rk_singleton_ge [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.set_of_points [definition, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.three_points_on_lines [axiom, in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProperties [moduleid, in ProjectiveGeometry.Space.rank_properties]
RankProperties.base_points_distinct_1 [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.base_points_distinct_2 [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.col_trans [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.construction [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.coplanar [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.couple_rk1 [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.couple_rk2 [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.couple_rk_degen [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.double_flag [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.eq_point_dec_rk [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.intersecting_lines_rank_3 [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.L1beta_gen [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.L1gamma_gen [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.Matroid' [moduleid, in ProjectiveGeometry.Space.rank_properties]
RankProperties.matroid3' [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.Mat_Props [moduleid, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rank_not_empty [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk2_3 [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk3_4 [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_compat [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_couple1 [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_couple2 [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_couple_not_zero [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_couple_1 [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_lemma_1 [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_couple_AB [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_couple_AC [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_couple_AD [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_couple_BC [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_couple_BD [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_couple_CD [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_triple_ABC [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_singleton [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_triple_ABC_couple_AB [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_triple_ABC_couple_AC [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_triple_ABC_couple_BC [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_triple_singleton [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.stays_in_plane [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.stays_in_the_plane [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.sym [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.uniq_inter [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.uniq_inter_spec [lemma, in ProjectiveGeometry.Space.rank_properties]
RankProperties.uniq_inter_spec_bis [lemma, in ProjectiveGeometry.Space.rank_properties]
rank_properties [library]
R_eq_dec [lemma, in ProjectiveGeometry.Plane.homogeneous]
R_eq_dec [lemma, in ProjectiveGeometry.Plane.moulton]


S

sets_of_points [library]
set01 [lemma, in ProjectiveGeometry.Plane.flat]
set12 [lemma, in ProjectiveGeometry.Plane.flat]
surj [definition, in ProjectiveGeometry.Plane.bij]
swap [moduleid, in ProjectiveGeometry.Plane.projective_plane_duality]
swapf3 [moduleid, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.A [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.ABF [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.ADG [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.B [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.BCD [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.BEG [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.C [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.CAE [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.CFG [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.D [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.DEF [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.E [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.F [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.G [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.Incid [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.is_fano_plane [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.is_fano_plane_inst [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.is_only_7_lines [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.is_only_7_pts [lemma, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.Line [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.Point [definition, in ProjectiveGeometry.Plane.fano_plane_desargues]
swap.a1_exist [definition, in ProjectiveGeometry.Plane.projective_plane_duality]
swap.a2_exist [definition, in ProjectiveGeometry.Plane.projective_plane_duality]
swap.a3_1 [definition, in ProjectiveGeometry.Plane.projective_plane_duality]
swap.a3_1_aux [lemma, in ProjectiveGeometry.Plane.projective_plane_duality]
swap.a3_2 [definition, in ProjectiveGeometry.Plane.projective_plane_duality]
swap.Incid [definition, in ProjectiveGeometry.Plane.projective_plane_duality]
swap.incid_dec [definition, in ProjectiveGeometry.Plane.projective_plane_duality]
swap.Line [definition, in ProjectiveGeometry.Plane.projective_plane_duality]
swap.M [moduleid, in ProjectiveGeometry.Plane.projective_plane_duality]
swap.Point [definition, in ProjectiveGeometry.Plane.projective_plane_duality]
swap.ProjectivePlaneFacts_m [moduleid, in ProjectiveGeometry.Plane.projective_plane_duality]
swap.uniq [moduleid, in ProjectiveGeometry.Plane.projective_plane_duality]
swap.uniqueness [lemma, in ProjectiveGeometry.Plane.projective_plane_duality]


T

test [lemma, in ProjectiveGeometry.Plane.hexamys]
test2 [lemma, in ProjectiveGeometry.Plane.hexamys]
test3 [lemma, in ProjectiveGeometry.Plane.hexamys]
test3' [lemma, in ProjectiveGeometry.Plane.hexamys]
test4 [lemma, in ProjectiveGeometry.Plane.hexamys]
test5 [lemma, in ProjectiveGeometry.Plane.hexamys]


U

uniq [moduleid, in ProjectiveGeometry.Plane.bij]
uniq [moduleid, in ProjectiveGeometry.Plane.examples]
uniq [moduleid, in ProjectiveGeometry.Plane.flat]
uniq [moduleid, in ProjectiveGeometry.Plane.hexamys]
uniqdec [moduleid, in ProjectiveGeometry.Plane.hexamys]
uniqueness_axioms [moduleid, in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.a1_exist [definition, in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.a1_unique [lemma, in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.a2_exist [definition, in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.a2_unique [lemma, in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.Incid [definition, in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.incidABl [lemma, in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.incidAl1l2 [lemma, in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.incid_dec [definition, in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.Line [definition, in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.Point [definition, in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.uniqueness [definition, in ProjectiveGeometry.Plane.basic_facts_plane]


V

VeblenYoungProjectiveSpace [moduleid, in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.A1 [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.A2 [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.A3 [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.collinear [definition, in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.E0 [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.E2 [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.Incid [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.Line [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.l0 [axiom, in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.Point [axiom, in ProjectiveGeometry.Space.projective_space_axioms]


Z

zero_neq_minus_one [lemma, in ProjectiveGeometry.Plane.homogeneous]
zero_neq_minus_one [lemma, in ProjectiveGeometry.Plane.moulton]



Lemma Index

A

almost_pappus [in ProjectiveGeometry.Plane.P05_almost_pappus]
angle_line [in ProjectiveGeometry.Plane.P06_angle_line]
a_chasles_th [in ProjectiveGeometry.Plane.P11_chasles]


B

back.case1 [in ProjectiveGeometry.Plane.back]
back.case2 [in ProjectiveGeometry.Plane.back]
back.case3 [in ProjectiveGeometry.Plane.back]
back.case4 [in ProjectiveGeometry.Plane.back]
BuildFSets.couple_singleton_eq [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.couple_1 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.inter_fsetdecide_1 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.inter_fsetdecide_2 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.inter_fsetdecide_4 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.inter_fsetdecide_5 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.subset_exists [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.test [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.test2 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.test_fsetdec [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.test_fsetdec2 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_couple_1 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_couple_2 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_couple_3 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_couple_4 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_couple_5 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_couple_6 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_1 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_2 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_3 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_4 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple_5 [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.union_fsetdecide [in ProjectiveGeometry.Space.sets_of_points]


C

c [in ProjectiveGeometry.Plane.examples]
cevian_lines [in ProjectiveGeometry.Plane.P07_cevian_lines]
cevian_lines_2 [in ProjectiveGeometry.Plane.P08_cevian_lines_2]
characterization [in ProjectiveGeometry.Plane.flat]
col_col_on_inter [in ProjectiveGeometry.Plane.hexamys]
col_comm [in ProjectiveGeometry.Plane.hexamys]
col_comm2 [in ProjectiveGeometry.Plane.hexamys]
col_comm3 [in ProjectiveGeometry.Plane.hexamys]
col_comm4 [in ProjectiveGeometry.Plane.hexamys]
col_comm5 [in ProjectiveGeometry.Plane.hexamys]
col_incid [in ProjectiveGeometry.Plane.hexamys]
col_line_eq [in ProjectiveGeometry.Plane.hexamys]
col_trivial_1 [in ProjectiveGeometry.Plane.hexamys]
col_trivial_2 [in ProjectiveGeometry.Plane.hexamys]
col_trivial_3 [in ProjectiveGeometry.Plane.hexamys]
complete_quadrilateral [in ProjectiveGeometry.Plane.P09_complete_quadrilateral]
complete_quadrilateral_2 [in ProjectiveGeometry.Plane.P10_complete_quadrilateral_2]


D

decidability.eq_line_dec [in ProjectiveGeometry.Plane.decidability]
decidability.eq_point_dec [in ProjectiveGeometry.Plane.decidability]
decidability.eq_point_dec_sublemma [in ProjectiveGeometry.Plane.decidability]
decidability.first_point [in ProjectiveGeometry.Plane.decidability]
decidability.incid_dec2 [in ProjectiveGeometry.Plane.decidability]
decidability.outsider [in ProjectiveGeometry.Plane.decidability]
decidability.second_line [in ProjectiveGeometry.Plane.decidability]
decidability.second_point [in ProjectiveGeometry.Plane.decidability]
decidability.third_point [in ProjectiveGeometry.Plane.decidability]
DesarguesxD.Desargues_xD [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.Desargues_xD' [in ProjectiveGeometry.Space.desarguesxD]
Desargues.Desargues [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues2Dfinal.Desargues_plane [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.rA'B'O' [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.rA'C'O' [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.rB'C'O' [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal2.Desargues_plane [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.new_scheme [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dlemmas.l1_scheme [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.l2rABMP_scheme [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rABCc_scheme [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rABCO [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rABOc_scheme [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rABOo_scheme [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rCC'oc_scheme [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rCC'oPc_scheme [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rcC'_scheme [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rcC_scheme [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rco_scheme [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rPcC'oO_scheme [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.rPC'oc_scheme [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.subl2rABMP_scheme [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas2.ex_o [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l1A'B'O [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l1A'C'O [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l1B'C'O [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l2rABMP [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l2rABOP [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l2rACMP [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.l2rA'B'OP [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.perm3 [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.ra [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rABCa [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rABCc [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rABCo [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rABOb [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rABOc [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rABOo [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rACMo [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rACOo [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rACOP [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rAO [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rao [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rA'B'Mo [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rA'B'Oo [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rA'C'Mo [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rA'C'Oo [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rA'C'OP [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rA'O [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rb [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rBCOP [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rbo [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rBO [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rB'C'OP [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rB'O [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rc [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rcC [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rcC' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rCC'oc [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rCC'oPc [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rco [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rCO [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.rC'O [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas3.beta_ok' [in ProjectiveGeometry.Space.desargues2Dlemmas3]
Desargues3DLemmas.A_not_beta_scheme [in ProjectiveGeometry.Space.desargues3Dlemmas]
Desargues3DLemmas.a_not_gamma_scheme [in ProjectiveGeometry.Space.desargues3Dlemmas]
Desargues3DLemmas.rbA_scheme [in ProjectiveGeometry.Space.desargues3Dlemmas]
Desargues3DLemmas.sublemma [in ProjectiveGeometry.Space.desargues3Dlemmas]
Desargues3DLemmas.sublemma'' [in ProjectiveGeometry.Space.desargues3Dlemmas]
Desargues3Dspecial.Desargues [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3D.A_not_alpha [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.a_not_alpha [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.A_not_beta [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.A_not_gamma [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.a_not_gamma [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.B_not_alpha [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.B_not_beta [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.b_not_gamma [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.B_not_gamma [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.C_not_alpha [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.C_not_beta [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.c_not_beta [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.C_not_gamma [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L1alpha [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L1palpha [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L1Pbeta [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L1pbeta [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L1pgamma [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L1Pgamma [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L2p [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.L2P [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rAB [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rab [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rac [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rAC [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.ralphabeta [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.ralphagamma [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rbc [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rBC [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rbetagamma [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.rPpalbega [in ProjectiveGeometry.Space.desargues3D]
desargues_cevian_case [in ProjectiveGeometry.Plane.hexamys_desargues]
Desargues_from_A.collinearPPQ [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.collinearPQP [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.collinearPQQ [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_degen_1 [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_degen_2 [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_degen_3 [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_1 [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_2 [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_3 [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_4 [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.col_5 [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.Desargues_from_A [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.Desargues_from_A_spec [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.not_all_equal [in ProjectiveGeometry.Plane.fano_plane_desargues]


E

eolien [in ProjectiveGeometry.Plane.P12_aeolian]
essai [in ProjectiveGeometry.Plane.hexamys]
example.dual_example [in ProjectiveGeometry.Plane.projective_plane_duality]


F

FanoPlane.a1_exist [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.a1_unique [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.a2_exist [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.a2_unique [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.a3 [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.degen_line [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.degen_point [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.incid_dec [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.uniqueness [in ProjectiveGeometry.Plane.fano_plane]
forth.cas1 [in ProjectiveGeometry.Plane.forth]
forth.cas2 [in ProjectiveGeometry.Plane.forth]
forth.cas3 [in ProjectiveGeometry.Plane.forth]
fp_empty [in ProjectiveGeometry.Plane.flat]
fp_line [in ProjectiveGeometry.Plane.flat]
fp_plane [in ProjectiveGeometry.Plane.flat]
fp_singleton [in ProjectiveGeometry.Plane.flat]


H

hexamy_desargues_gen_case [in ProjectiveGeometry.Plane.hexamys_desargues]
hexamy_prop [in ProjectiveGeometry.Plane.hexamys]
hexamy_rot_left [in ProjectiveGeometry.Plane.hexamys]
hexamy_rot_right [in ProjectiveGeometry.Plane.hexamys]
hexamy_special_case [in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_right [in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_2_3 [in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_2_4 [in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_2_5 [in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_2_6 [in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_3_4 [in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_3_5 [in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_3_6 [in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_4_5 [in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_4_6 [in ProjectiveGeometry.Plane.hexamys]
hexamy_swap_5_6 [in ProjectiveGeometry.Plane.hexamys]
HomogenousCoords.a1_exist [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.a2_exist [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.a3_1 [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.a3_2 [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.equiv_and [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.equiv_eq [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.equiv_or [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.eq_point_dec [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.eq_1 [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.eq_2 [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.incid_dec [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.normalize_compat_incid [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.point_of_triple_functionnal [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.point_triple [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.triple_point [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.uniqueness [in ProjectiveGeometry.Plane.homogeneous]


I

incid_inter_left [in ProjectiveGeometry.Plane.hexamys]
incid_inter_right [in ProjectiveGeometry.Plane.hexamys]
incid_line_left [in ProjectiveGeometry.Plane.hexamys]
incid_line_right [in ProjectiveGeometry.Plane.hexamys]
Incid_property [in ProjectiveGeometry.Plane.examples]
included_or_not [in ProjectiveGeometry.Plane.flat]
inter_comm [in ProjectiveGeometry.Plane.hexamys]
is_on_proper_inter_is_on_inter [in ProjectiveGeometry.Plane.hexamys]


L

Lc [in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lc [in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcdiv1 [in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcdiv1 [in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcdiv2 [in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcdiv2 [in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcinv [in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcinv [in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcmult1 [in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcmult1 [in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcmult2 [in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcmult2 [in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcm1 [in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcm1 [in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcm2 [in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcm2 [in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcop1 [in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcop1 [in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcp1 [in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcp1 [in ProjectiveGeometry.Space.field_variable_isolation_tactic]
Lcp2 [in ProjectiveGeometry.Plane.field_variable_isolation_tactic]
Lcp2 [in ProjectiveGeometry.Space.field_variable_isolation_tactic]
line_comm [in ProjectiveGeometry.Plane.hexamys]
line_neq_neq [in ProjectiveGeometry.Plane.hexamys]
line_set_of_points [in ProjectiveGeometry.Plane.bij]
line_wd [in ProjectiveGeometry.Plane.hexamys]
line_wd_sym [in ProjectiveGeometry.Plane.hexamys]


M

Matroid_Properties.add_inj [in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.cardinal_couple [in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.eq_point_dec [in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.matroid1_b_useful [in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.matroid3'_gen [in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.matroid3_useful [in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.rk_couple_2 [in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.rk_quadruple_le [in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.rk_singleton_le [in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.rk_triple_le [in ProjectiveGeometry.Space.matroids_properties]
matroid_to_matroid'.add_union_singleton_sym [in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.matroid1' [in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.matroid2' [in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.matroid3' [in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.matroid3_useful [in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.rk_compat [in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.rk_singleton [in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.test_fsetdec [in ProjectiveGeometry.Space.matroid_to_matroid_p]
Moulton.a1_exist [in ProjectiveGeometry.Plane.moulton]
Moulton.a2_exist [in ProjectiveGeometry.Plane.moulton]
Moulton.a3_1 [in ProjectiveGeometry.Plane.moulton]
Moulton.a3_2 [in ProjectiveGeometry.Plane.moulton]
Moulton.equiv_and [in ProjectiveGeometry.Plane.moulton]
Moulton.equiv_eq [in ProjectiveGeometry.Plane.moulton]
Moulton.equiv_or [in ProjectiveGeometry.Plane.moulton]
Moulton.eq_point_dec [in ProjectiveGeometry.Plane.moulton]
Moulton.foo [in ProjectiveGeometry.Plane.moulton]
Moulton.hint0 [in ProjectiveGeometry.Plane.moulton]
Moulton.hint1 [in ProjectiveGeometry.Plane.moulton]
Moulton.hint2 [in ProjectiveGeometry.Plane.moulton]
Moulton.hint2' [in ProjectiveGeometry.Plane.moulton]
Moulton.hint2'' [in ProjectiveGeometry.Plane.moulton]
Moulton.hint3 [in ProjectiveGeometry.Plane.moulton]
Moulton.hint4 [in ProjectiveGeometry.Plane.moulton]
Moulton.hint5 [in ProjectiveGeometry.Plane.moulton]
Moulton.hint6 [in ProjectiveGeometry.Plane.moulton]
Moulton.hint7 [in ProjectiveGeometry.Plane.moulton]
Moulton.incid_dec [in ProjectiveGeometry.Plane.moulton]
Moulton.is_equiv [in ProjectiveGeometry.Plane.moulton]
Moulton.non_desarguesian [in ProjectiveGeometry.Plane.moulton]
Moulton.normalize_not [in ProjectiveGeometry.Plane.moulton]
Moulton.strict_or_not [in ProjectiveGeometry.Plane.moulton]
Moulton.sub_lemma1 [in ProjectiveGeometry.Plane.moulton]
Moulton.sub_lemma2 [in ProjectiveGeometry.Plane.moulton]
Moulton.sub_lemma3 [in ProjectiveGeometry.Plane.moulton]
Moulton.sub_lemma4 [in ProjectiveGeometry.Plane.moulton]
Moulton.sys_eqs_1 [in ProjectiveGeometry.Plane.moulton]
Moulton.sys_eqs_2 [in ProjectiveGeometry.Plane.moulton]
Moulton.sys_eqs_3 [in ProjectiveGeometry.Plane.moulton]
Moulton.sys_eqs_4 [in ProjectiveGeometry.Plane.moulton]
Moulton.uniqueness [in ProjectiveGeometry.Plane.moulton]


N

not_eq_sym_line [in ProjectiveGeometry.Plane.hexamys]
not_eq_sym_point [in ProjectiveGeometry.Plane.hexamys]


O

one_not_two [in ProjectiveGeometry.Plane.homogeneous]
one_not_two [in ProjectiveGeometry.Plane.moulton]
on_inter_points_wd [in ProjectiveGeometry.Plane.hexamys]
on_inter_points_wd_spec_1 [in ProjectiveGeometry.Plane.hexamys]
on_inter_points_wd_spec_2 [in ProjectiveGeometry.Plane.hexamys]
on_inter_points_wd_spec_3 [in ProjectiveGeometry.Plane.hexamys]
on_inter_points_wd_spec_4 [in ProjectiveGeometry.Plane.hexamys]
on_inter_wd [in ProjectiveGeometry.Plane.hexamys]
on_inter_wd_sym [in ProjectiveGeometry.Plane.hexamys]


P

pappus_pappus_strong [in ProjectiveGeometry.Plane.hexamys]
PG25.a1_exist [in ProjectiveGeometry.Plane.pg25]
PG25.a2_exist [in ProjectiveGeometry.Plane.pg25]
PG25.a3 [in ProjectiveGeometry.Plane.pg25]
PG25.incid_dec [in ProjectiveGeometry.Plane.pg25]
PG25.uniqueness [in ProjectiveGeometry.Plane.pg25]
ProjectivePlane2HeytingProjectivePlane.P1 [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.P2 [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.P3 [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.P4 [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.P5i [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.P5ii [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.P5iii [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.S1 [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.S2 [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.S3 [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectiveSpaceFacts.a1_unique [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.a2_unique [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.a3_3simplified [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.eq_line_dec [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.incidABl [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.incidAl1l2 [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.only_one_intersection [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.second_line [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.second_point [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.third_line [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.third_point [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.two_lines_aux [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.two_lines_P [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.two_points_not_incident_l1l2 [in ProjectiveGeometry.Space.basic_facts]
pset_decompose [in ProjectiveGeometry.Plane.flat]
pseudo_midpoint [in ProjectiveGeometry.Plane.P14_pseudo_midpoint]


R

RankProjectiveSpaceToProjectiveSpaceOrHigher.a1_exists [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.a2 [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.a3_1 [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.a3_2 [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.incid_dec [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.line_eq_refl [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.line_eq_sym [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.line_eq_trans [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.second_point [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.uniqueness [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProperties.base_points_distinct_1 [in ProjectiveGeometry.Space.rank_properties]
RankProperties.base_points_distinct_2 [in ProjectiveGeometry.Space.rank_properties]
RankProperties.col_trans [in ProjectiveGeometry.Space.rank_properties]
RankProperties.construction [in ProjectiveGeometry.Space.rank_properties]
RankProperties.coplanar [in ProjectiveGeometry.Space.rank_properties]
RankProperties.couple_rk1 [in ProjectiveGeometry.Space.rank_properties]
RankProperties.couple_rk2 [in ProjectiveGeometry.Space.rank_properties]
RankProperties.couple_rk_degen [in ProjectiveGeometry.Space.rank_properties]
RankProperties.double_flag [in ProjectiveGeometry.Space.rank_properties]
RankProperties.eq_point_dec_rk [in ProjectiveGeometry.Space.rank_properties]
RankProperties.intersecting_lines_rank_3 [in ProjectiveGeometry.Space.rank_properties]
RankProperties.L1beta_gen [in ProjectiveGeometry.Space.rank_properties]
RankProperties.L1gamma_gen [in ProjectiveGeometry.Space.rank_properties]
RankProperties.matroid3' [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rank_not_empty [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk2_3 [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk3_4 [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_compat [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_couple1 [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_couple2 [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_couple_not_zero [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_couple_1 [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_lemma_1 [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_couple_AB [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_couple_AC [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_couple_AD [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_couple_BC [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_couple_BD [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_couple_CD [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_quadruple_ABCD_triple_ABC [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_singleton [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_triple_ABC_couple_AB [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_triple_ABC_couple_AC [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_triple_ABC_couple_BC [in ProjectiveGeometry.Space.rank_properties]
RankProperties.rk_triple_singleton [in ProjectiveGeometry.Space.rank_properties]
RankProperties.stays_in_plane [in ProjectiveGeometry.Space.rank_properties]
RankProperties.stays_in_the_plane [in ProjectiveGeometry.Space.rank_properties]
RankProperties.sym [in ProjectiveGeometry.Space.rank_properties]
RankProperties.uniq_inter [in ProjectiveGeometry.Space.rank_properties]
RankProperties.uniq_inter_spec [in ProjectiveGeometry.Space.rank_properties]
RankProperties.uniq_inter_spec_bis [in ProjectiveGeometry.Space.rank_properties]
R_eq_dec [in ProjectiveGeometry.Plane.homogeneous]
R_eq_dec [in ProjectiveGeometry.Plane.moulton]


S

set01 [in ProjectiveGeometry.Plane.flat]
set12 [in ProjectiveGeometry.Plane.flat]
swapf3.is_fano_plane_inst [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.is_only_7_lines [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.is_only_7_pts [in ProjectiveGeometry.Plane.fano_plane_desargues]
swap.a3_1_aux [in ProjectiveGeometry.Plane.projective_plane_duality]
swap.uniqueness [in ProjectiveGeometry.Plane.projective_plane_duality]


T

test [in ProjectiveGeometry.Plane.hexamys]
test2 [in ProjectiveGeometry.Plane.hexamys]
test3 [in ProjectiveGeometry.Plane.hexamys]
test3' [in ProjectiveGeometry.Plane.hexamys]
test4 [in ProjectiveGeometry.Plane.hexamys]
test5 [in ProjectiveGeometry.Plane.hexamys]


U

uniqueness_axioms.a1_unique [in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.a2_unique [in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.incidABl [in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.incidAl1l2 [in ProjectiveGeometry.Plane.basic_facts_plane]


Z

zero_neq_minus_one [in ProjectiveGeometry.Plane.homogeneous]
zero_neq_minus_one [in ProjectiveGeometry.Plane.moulton]



Section Index

D

DesarguesxD.desargues_theorem [in ProjectiveGeometry.Space.desarguesxD]
Desargues2Dfinal.desargues_theorem [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal2.desargues_theorem [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dlemmas2.desargues_plane [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.a_exists [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.b_exists [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.c_exists [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues3Dspecial.Desargues [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3D.Desargues_general [in ProjectiveGeometry.Space.desargues3D]



Constructor Index

F

FanoPlane.A [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.ABF [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.ADG [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.B [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.BCD [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.BEG [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.C [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.CAE [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.CFG [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.D [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.DEF [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.E [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.F [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.G [in ProjectiveGeometry.Plane.fano_plane]


H

HomogenousCoords.L0 [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.L1 [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.L2 [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.P0 [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.P1 [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.P2 [in ProjectiveGeometry.Plane.homogeneous]


M

Moulton.dir [in ProjectiveGeometry.Plane.moulton]
Moulton.Infinite [in ProjectiveGeometry.Plane.moulton]
Moulton.L [in ProjectiveGeometry.Plane.moulton]
Moulton.P [in ProjectiveGeometry.Plane.moulton]


P

PG25.l0 [in ProjectiveGeometry.Plane.pg25]
PG25.l1 [in ProjectiveGeometry.Plane.pg25]
PG25.l10 [in ProjectiveGeometry.Plane.pg25]
PG25.l11 [in ProjectiveGeometry.Plane.pg25]
PG25.l12 [in ProjectiveGeometry.Plane.pg25]
PG25.l13 [in ProjectiveGeometry.Plane.pg25]
PG25.l14 [in ProjectiveGeometry.Plane.pg25]
PG25.l15 [in ProjectiveGeometry.Plane.pg25]
PG25.l16 [in ProjectiveGeometry.Plane.pg25]
PG25.l17 [in ProjectiveGeometry.Plane.pg25]
PG25.l18 [in ProjectiveGeometry.Plane.pg25]
PG25.l19 [in ProjectiveGeometry.Plane.pg25]
PG25.l2 [in ProjectiveGeometry.Plane.pg25]
PG25.l20 [in ProjectiveGeometry.Plane.pg25]
PG25.l21 [in ProjectiveGeometry.Plane.pg25]
PG25.l22 [in ProjectiveGeometry.Plane.pg25]
PG25.l23 [in ProjectiveGeometry.Plane.pg25]
PG25.l24 [in ProjectiveGeometry.Plane.pg25]
PG25.l25 [in ProjectiveGeometry.Plane.pg25]
PG25.l26 [in ProjectiveGeometry.Plane.pg25]
PG25.l27 [in ProjectiveGeometry.Plane.pg25]
PG25.l28 [in ProjectiveGeometry.Plane.pg25]
PG25.l29 [in ProjectiveGeometry.Plane.pg25]
PG25.l3 [in ProjectiveGeometry.Plane.pg25]
PG25.l30 [in ProjectiveGeometry.Plane.pg25]
PG25.l4 [in ProjectiveGeometry.Plane.pg25]
PG25.l5 [in ProjectiveGeometry.Plane.pg25]
PG25.l6 [in ProjectiveGeometry.Plane.pg25]
PG25.l7 [in ProjectiveGeometry.Plane.pg25]
PG25.l8 [in ProjectiveGeometry.Plane.pg25]
PG25.l9 [in ProjectiveGeometry.Plane.pg25]
PG25.P0 [in ProjectiveGeometry.Plane.pg25]
PG25.P1 [in ProjectiveGeometry.Plane.pg25]
PG25.P10 [in ProjectiveGeometry.Plane.pg25]
PG25.P11 [in ProjectiveGeometry.Plane.pg25]
PG25.P12 [in ProjectiveGeometry.Plane.pg25]
PG25.P13 [in ProjectiveGeometry.Plane.pg25]
PG25.P14 [in ProjectiveGeometry.Plane.pg25]
PG25.P15 [in ProjectiveGeometry.Plane.pg25]
PG25.P16 [in ProjectiveGeometry.Plane.pg25]
PG25.P17 [in ProjectiveGeometry.Plane.pg25]
PG25.P18 [in ProjectiveGeometry.Plane.pg25]
PG25.P19 [in ProjectiveGeometry.Plane.pg25]
PG25.P2 [in ProjectiveGeometry.Plane.pg25]
PG25.P20 [in ProjectiveGeometry.Plane.pg25]
PG25.P21 [in ProjectiveGeometry.Plane.pg25]
PG25.P22 [in ProjectiveGeometry.Plane.pg25]
PG25.P23 [in ProjectiveGeometry.Plane.pg25]
PG25.P24 [in ProjectiveGeometry.Plane.pg25]
PG25.P25 [in ProjectiveGeometry.Plane.pg25]
PG25.P26 [in ProjectiveGeometry.Plane.pg25]
PG25.P27 [in ProjectiveGeometry.Plane.pg25]
PG25.P28 [in ProjectiveGeometry.Plane.pg25]
PG25.P29 [in ProjectiveGeometry.Plane.pg25]
PG25.P3 [in ProjectiveGeometry.Plane.pg25]
PG25.P30 [in ProjectiveGeometry.Plane.pg25]
PG25.P4 [in ProjectiveGeometry.Plane.pg25]
PG25.P5 [in ProjectiveGeometry.Plane.pg25]
PG25.P6 [in ProjectiveGeometry.Plane.pg25]
PG25.P7 [in ProjectiveGeometry.Plane.pg25]
PG25.P8 [in ProjectiveGeometry.Plane.pg25]
PG25.P9 [in ProjectiveGeometry.Plane.pg25]


R

RankProjectiveSpaceToProjectiveSpaceOrHigher.Cline [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]



Inductive Index

F

FanoPlane.ind_line [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.ind_Point [in ProjectiveGeometry.Plane.fano_plane]


H

HomogenousCoords.IndLine [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.IndPoint [in ProjectiveGeometry.Plane.homogeneous]


M

Moulton.IndLine [in ProjectiveGeometry.Plane.moulton]
Moulton.IndPoint [in ProjectiveGeometry.Plane.moulton]


P

PG25.ind_line [in ProjectiveGeometry.Plane.pg25]
PG25.ind_point [in ProjectiveGeometry.Plane.pg25]


R

RankProjectiveSpaceToProjectiveSpaceOrHigher.LineInd [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]



Definition Index

B

back.a1_exist [in ProjectiveGeometry.Plane.back]
back.a2_exist [in ProjectiveGeometry.Plane.back]
back.a3 [in ProjectiveGeometry.Plane.back]
back.Incid [in ProjectiveGeometry.Plane.back]
back.incid_dec [in ProjectiveGeometry.Plane.back]
back.Line [in ProjectiveGeometry.Plane.back]
back.Point [in ProjectiveGeometry.Plane.back]
back.uniqueness [in ProjectiveGeometry.Plane.back]
bij [in ProjectiveGeometry.Plane.bij]
BuildFSets.couple [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.Point [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.quadruple [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.set_of_points [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.triple [in ProjectiveGeometry.Space.sets_of_points]


C

cevian_in [in ProjectiveGeometry.Plane.P07_cevian_lines]
Col [in ProjectiveGeometry.Plane.hexamys]
Col_on [in ProjectiveGeometry.Plane.hexamys]
CoxeterProjectivePlane.bijective [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.collinear [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.injective [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.is_elementary_projectivity [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.is_inter [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.is_perspectivity [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.surjective [in ProjectiveGeometry.Plane.projective_plane_axioms]


D

decidability.Incid [in ProjectiveGeometry.Plane.decidability]
decidability.Line [in ProjectiveGeometry.Plane.decidability]
decidability.Point [in ProjectiveGeometry.Plane.decidability]
Desargues3D.Ps [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.ps [in ProjectiveGeometry.Space.desargues3D]
Desargues_from_A.collinear [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues_from_A.on_line [in ProjectiveGeometry.Plane.fano_plane_desargues]
dist3 [in ProjectiveGeometry.Plane.general_tactics]
dist3 [in ProjectiveGeometry.Space.general_tactics]
dist4 [in ProjectiveGeometry.Plane.general_tactics]
dist4 [in ProjectiveGeometry.Space.general_tactics]
dist6 [in ProjectiveGeometry.Plane.general_tactics]
dist_3 [in ProjectiveGeometry.Space.projective_space_axioms]
dist_4 [in ProjectiveGeometry.Space.projective_space_axioms]


F

FanoPlane.Incid [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.Incid_bool [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.Line [in ProjectiveGeometry.Plane.fano_plane]
FanoPlane.Point [in ProjectiveGeometry.Plane.fano_plane]
fano_plane.is_fano_plane [in ProjectiveGeometry.Plane.fano_plane_desargues]
flat [in ProjectiveGeometry.Plane.flat]
forth.a1_exist [in ProjectiveGeometry.Plane.forth]
forth.a2_exist [in ProjectiveGeometry.Plane.forth]
forth.a3_1 [in ProjectiveGeometry.Plane.forth]
forth.a3_2 [in ProjectiveGeometry.Plane.forth]
forth.Incid [in ProjectiveGeometry.Plane.forth]
forth.incid_dec [in ProjectiveGeometry.Plane.forth]
forth.Line [in ProjectiveGeometry.Plane.forth]
forth.Point [in ProjectiveGeometry.Plane.forth]
forth.uniqueness [in ProjectiveGeometry.Plane.forth]


H

hexamy [in ProjectiveGeometry.Plane.hexamys]
HeytingProjectivePlane.apart_l [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.out [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HomogenousCoords.det2 [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.general_line_through [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.general_point_through [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.Incid [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.Incid_triple [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.inner_product_triple [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.Line [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.line_of_triple [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.Point [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.point_of_triple [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.triple_of_line [in ProjectiveGeometry.Plane.homogeneous]
HomogenousCoords.triple_of_point [in ProjectiveGeometry.Plane.homogeneous]


I

inj [in ProjectiveGeometry.Plane.bij]
inter [in ProjectiveGeometry.Plane.hexamys]
is_hexamy [in ProjectiveGeometry.Plane.hexamys]
is_on_inter [in ProjectiveGeometry.Plane.hexamys]
is_on_proper_inter [in ProjectiveGeometry.Plane.hexamys]
is_transverse [in ProjectiveGeometry.Plane.hexamys]


L

line [in ProjectiveGeometry.Plane.hexamys]
line_as_set_of_points [in ProjectiveGeometry.Plane.bij]


M

matroid_to_matroid'.rk [in ProjectiveGeometry.Space.matroid_to_matroid_p]
Meet [in ProjectiveGeometry.Plane.hexamys]
Moulton.collinear [in ProjectiveGeometry.Plane.moulton]
Moulton.Incid [in ProjectiveGeometry.Plane.moulton]
Moulton.Line [in ProjectiveGeometry.Plane.moulton]
Moulton.non_collinear [in ProjectiveGeometry.Plane.moulton]
Moulton.on_line [in ProjectiveGeometry.Plane.moulton]
Moulton.Point [in ProjectiveGeometry.Plane.moulton]


O

on_inter [in ProjectiveGeometry.Plane.hexamys]
on_inter' [in ProjectiveGeometry.Plane.hexamys]


P

pappus_strong [in ProjectiveGeometry.Plane.hexamys]
pappus_weak [in ProjectiveGeometry.Plane.hexamys]
pempty [in ProjectiveGeometry.Plane.flat]
PG25.Incid [in ProjectiveGeometry.Plane.pg25]
PG25.Incid_bool [in ProjectiveGeometry.Plane.pg25]
PG25.Line [in ProjectiveGeometry.Plane.pg25]
PG25.Point [in ProjectiveGeometry.Plane.pg25]
pline [in ProjectiveGeometry.Plane.flat]
pplane [in ProjectiveGeometry.Plane.flat]
ProjectivePlane2HeytingProjectivePlane.Apart [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.apart_l [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.Incid [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.Line [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.out [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.Point [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectiveSpaceFacts.Incid [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.Line [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceFacts.Point [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceOrHigher.dist3 [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.dist4 [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.Point [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.dist3 [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.dist4 [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.Intersect [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.Intersect_In [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.Point [in ProjectiveGeometry.Space.projective_space_axioms]
pset [in ProjectiveGeometry.Plane.flat]
psingleton [in ProjectiveGeometry.Plane.flat]


R

RankProjectiveSpaceToProjectiveSpaceOrHigher.dist3 [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.dist4 [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.fstP [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.Incid [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.Line [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.line_eq [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.Point [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.sndP [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpace.Point [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.set_of_points [in ProjectiveGeometry.Space.projective_space_rank_axioms]


S

surj [in ProjectiveGeometry.Plane.bij]
swapf3.A [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.ABF [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.ADG [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.B [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.BCD [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.BEG [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.C [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.CAE [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.CFG [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.D [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.DEF [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.E [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.F [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.G [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.Incid [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.is_fano_plane [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.Line [in ProjectiveGeometry.Plane.fano_plane_desargues]
swapf3.Point [in ProjectiveGeometry.Plane.fano_plane_desargues]
swap.a1_exist [in ProjectiveGeometry.Plane.projective_plane_duality]
swap.a2_exist [in ProjectiveGeometry.Plane.projective_plane_duality]
swap.a3_1 [in ProjectiveGeometry.Plane.projective_plane_duality]
swap.a3_2 [in ProjectiveGeometry.Plane.projective_plane_duality]
swap.Incid [in ProjectiveGeometry.Plane.projective_plane_duality]
swap.incid_dec [in ProjectiveGeometry.Plane.projective_plane_duality]
swap.Line [in ProjectiveGeometry.Plane.projective_plane_duality]
swap.Point [in ProjectiveGeometry.Plane.projective_plane_duality]


U

uniqueness_axioms.a1_exist [in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.a2_exist [in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.Incid [in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.incid_dec [in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.Line [in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.Point [in ProjectiveGeometry.Plane.basic_facts_plane]
uniqueness_axioms.uniqueness [in ProjectiveGeometry.Plane.basic_facts_plane]


V

VeblenYoungProjectiveSpace.collinear [in ProjectiveGeometry.Space.projective_space_axioms]



Axiom Index

A

AbstractProjectivePlane.a1_exist [in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.a2_exist [in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.a3 [in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.Incid [in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.incid_dec [in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.Line [in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.Point [in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane.uniqueness [in ProjectiveGeometry.Plane.projective_plane_inst]


C

CoherentProjectivePlane.a1_exist [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.a2_exist [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.a3_1 [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.a3_2 [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.Incid [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.incid_dec [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.Line [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.l1 [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.l2 [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.Point [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoherentProjectivePlane.uniqueness [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.a1_unique [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.a2_exist [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.a2_17 [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.a3 [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.Incid [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.incid_dec [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.Line [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.l2_18 [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane.Point [in ProjectiveGeometry.Plane.projective_plane_axioms]


D

Decidability.eq_line_dec [in ProjectiveGeometry.Plane.decidability]
Decidability.eq_point_dec [in ProjectiveGeometry.Plane.decidability]
Decidability.Incid [in ProjectiveGeometry.Plane.decidability]
Decidability.Line [in ProjectiveGeometry.Plane.decidability]
Decidability.outsider [in ProjectiveGeometry.Plane.decidability]
Decidability.Point [in ProjectiveGeometry.Plane.decidability]


F

fano_plane.is_fano_plane_inst [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.is_only_7_lines [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.is_only_7_pts [in ProjectiveGeometry.Plane.fano_plane_desargues]


H

HeytingProjectivePlane.Apart [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.Incid [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.Line [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.Point [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P1 [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P2 [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P3 [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P4 [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P5i [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P5ii [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.P5iii [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.S1 [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.S2 [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HeytingProjectivePlane.S3 [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]


M

Matroid'.matroid1' [in ProjectiveGeometry.Space.matroids_axioms]
Matroid'.matroid2' [in ProjectiveGeometry.Space.matroids_axioms]
Matroid'.matroid3' [in ProjectiveGeometry.Space.matroids_axioms]
Matroid'.rk [in ProjectiveGeometry.Space.matroids_axioms]
Matroid'.rk_compat [in ProjectiveGeometry.Space.matroids_axioms]
Matroid.matroid1_a [in ProjectiveGeometry.Space.matroids_axioms]
Matroid.matroid1_b [in ProjectiveGeometry.Space.matroids_axioms]
Matroid.matroid2 [in ProjectiveGeometry.Space.matroids_axioms]
Matroid.matroid3 [in ProjectiveGeometry.Space.matroids_axioms]
Matroid.rk [in ProjectiveGeometry.Space.matroids_axioms]
Moulton.R_pos_neg [in ProjectiveGeometry.Plane.moulton]


P

PreProjectivePlane.a1_exist [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane.a2_exist [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane.Incid [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane.incid_dec [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane.Line [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane.Point [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane.uniqueness [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.a1_exist [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.a1_unique [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.a2_exist [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.a2_unique [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.Incid [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.incidABl [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.incidAl1l2 [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.incid_dec [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.Line [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.Point [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2.uniqueness [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.a1_exist [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.a2_exist [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.a3_1 [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.a3_2 [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.Incid [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.incid_dec [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.Line [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.Point [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane'.uniqueness [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.a1_exist [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.a2_exist [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.a3 [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.Incid [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.incid_dec [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.Line [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.Point [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane.uniqueness [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.a1_exist [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.a1_unique [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.a2_exist [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.a2_unique [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.a3_1 [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.a3_2 [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.Incid [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.incid_dec [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.Line [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2.Point [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectiveSpaceFacts.Incid_mor [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceOrHigher.a1_exists [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.a2 [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.a3_1 [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.a3_2 [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.Incid [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.incid_dec [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.Line [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.line_eq [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.line_eq_refl [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.line_eq_sym [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.line_eq_trans [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceOrHigher.uniqueness [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.a1_exists [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.a2 [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.a3_1 [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.a3_2 [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.a3_3 [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.Incid [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.incid_dec [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.Line [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpace.uniqueness [in ProjectiveGeometry.Space.projective_space_axioms]
proof_irr [in ProjectiveGeometry.Plane.bij]


R

RankProjectiveSpace.lower_dim [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.matroid1_a [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.matroid1_b [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.matroid2 [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.matroid3 [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.pasch [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.P0 [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.P1 [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.P2 [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.P3 [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.rk [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.rk_couple_ge [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.rk_singleton_ge [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpace.three_points_on_lines [in ProjectiveGeometry.Space.projective_space_rank_axioms]


V

VeblenYoungProjectiveSpace.A1 [in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.A2 [in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.A3 [in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.E0 [in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.E2 [in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.Incid [in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.Line [in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.l0 [in ProjectiveGeometry.Space.projective_space_axioms]
VeblenYoungProjectiveSpace.Point [in ProjectiveGeometry.Space.projective_space_axioms]



Moduleid Index

A

AbstractProjectivePlane [in ProjectiveGeometry.Plane.projective_plane_inst]
AbstractProjectivePlane' [in ProjectiveGeometry.Plane.projective_plane_inst]


B

back [in ProjectiveGeometry.Plane.back]
back.uniq [in ProjectiveGeometry.Plane.back]
BuildFSets [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.Dec [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.FiniteSetsOfPoints [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.FiniteSetsOfPointsProperties [in ProjectiveGeometry.Space.sets_of_points]
BuildFSets.FM [in ProjectiveGeometry.Space.sets_of_points]


C

CoherentProjectivePlane [in ProjectiveGeometry.Plane.projective_plane_axioms]
CoxeterProjectivePlane [in ProjectiveGeometry.Plane.projective_plane_axioms]


D

decid [in ProjectiveGeometry.Plane.flat]
decid [in ProjectiveGeometry.Plane.bij]
decidability [in ProjectiveGeometry.Plane.decidability]
Decidability [in ProjectiveGeometry.Plane.decidability]
decidability.ProjectivePlane' [in ProjectiveGeometry.Plane.decidability]
decidability.uniq [in ProjectiveGeometry.Plane.decidability]
Desargues [in ProjectiveGeometry.Plane.fano_plane_desargues]
DesarguesxD [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.Desargues_2D [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.Desargues_3D [in ProjectiveGeometry.Space.desarguesxD]
Desargues.M2 [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_B [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_B' [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_C [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_C' [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_D [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_D' [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_E [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_E' [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_F [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_F' [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_G [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues.swaped_G' [in ProjectiveGeometry.Plane.fano_plane_desargues]
Desargues2Dfinal [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.Desargues_2D_lem3 [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.Desargues_3D [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal2 [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.Desargues_2D_final [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dlemmas [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas.Props [in ProjectiveGeometry.Space.desargues2Dlemmas]
Desargues2Dlemmas2 [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.Desargues_plane_lem [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas3 [in ProjectiveGeometry.Space.desargues2Dlemmas3]
Desargues2Dlemmas3.Desargues_plane_lem [in ProjectiveGeometry.Space.desargues2Dlemmas3]
Desargues2Dlemmas3.Desargues_plane_lem2 [in ProjectiveGeometry.Space.desargues2Dlemmas3]
Desargues3D [in ProjectiveGeometry.Space.desargues3D]
Desargues3DLemmas [in ProjectiveGeometry.Space.desargues3Dlemmas]
Desargues3DLemmas.Props [in ProjectiveGeometry.Space.desargues3Dlemmas]
Desargues3Dspecial [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues3D [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3D.Desargues3DLemmas [in ProjectiveGeometry.Space.desargues3D]
Desargues_from_A [in ProjectiveGeometry.Plane.fano_plane_desargues]


E

example [in ProjectiveGeometry.Plane.projective_plane_duality]
example.Swaped [in ProjectiveGeometry.Plane.projective_plane_duality]


F

FanoPlane [in ProjectiveGeometry.Plane.fano_plane]
fano_plane [in ProjectiveGeometry.Plane.fano_plane_desargues]
forth [in ProjectiveGeometry.Plane.forth]
forth.uniq [in ProjectiveGeometry.Plane.forth]


H

HeytingProjectivePlane [in ProjectiveGeometry.Plane.Heyting_projective_plane_axioms]
HomogenousCoords [in ProjectiveGeometry.Plane.homogeneous]


M

Matroid [in ProjectiveGeometry.Space.matroids_axioms]
Matroid' [in ProjectiveGeometry.Space.matroids_axioms]
Matroid'.FiniteSetsDefs [in ProjectiveGeometry.Space.matroids_axioms]
Matroid.FiniteSetsDefs [in ProjectiveGeometry.Space.matroids_axioms]
Matroid_Properties [in ProjectiveGeometry.Space.matroids_properties]
Matroid_Properties.M' [in ProjectiveGeometry.Space.matroids_properties]
matroid_to_matroid' [in ProjectiveGeometry.Space.matroid_to_matroid_p]
matroid_to_matroid'.FiniteSetsDefs [in ProjectiveGeometry.Space.matroid_to_matroid_p]
Moulton [in ProjectiveGeometry.Plane.moulton]


P

PG25 [in ProjectiveGeometry.Plane.pg25]
PreProjectivePlane [in ProjectiveGeometry.Plane.projective_plane_axioms]
PreProjectivePlane2 [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane' [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2 [in ProjectiveGeometry.Plane.projective_plane_axioms]
ProjectivePlane2HeytingProjectivePlane [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.Facts [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.M' [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectivePlane2HeytingProjectivePlane.uniq [in ProjectiveGeometry.Plane.projective_plane_to_Heyting_projective_plane]
ProjectiveSpace [in ProjectiveGeometry.Space.projective_space_axioms]
ProjectiveSpaceFacts [in ProjectiveGeometry.Space.basic_facts]
ProjectiveSpaceOrHigher [in ProjectiveGeometry.Space.projective_space_axioms]


R

RankProjectiveSpace [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProjectiveSpaceToProjectiveSpaceOrHigher [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpaceToProjectiveSpaceOrHigher.Props [in ProjectiveGeometry.Space.projective_space_rank_to_projective_space]
RankProjectiveSpace.FiniteSetsDefs [in ProjectiveGeometry.Space.projective_space_rank_axioms]
RankProperties [in ProjectiveGeometry.Space.rank_properties]
RankProperties.Matroid' [in ProjectiveGeometry.Space.rank_properties]
RankProperties.Mat_Props [in ProjectiveGeometry.Space.rank_properties]


S

swap [in ProjectiveGeometry.Plane.projective_plane_duality]
swapf3 [in ProjectiveGeometry.Plane.fano_plane_desargues]
swap.M [in ProjectiveGeometry.Plane.projective_plane_duality]
swap.ProjectivePlaneFacts_m [in ProjectiveGeometry.Plane.projective_plane_duality]
swap.uniq [in ProjectiveGeometry.Plane.projective_plane_duality]


U

uniq [in ProjectiveGeometry.Plane.bij]
uniq [in ProjectiveGeometry.Plane.examples]
uniq [in ProjectiveGeometry.Plane.flat]
uniq [in ProjectiveGeometry.Plane.hexamys]
uniqdec [in ProjectiveGeometry.Plane.hexamys]
uniqueness_axioms [in ProjectiveGeometry.Plane.basic_facts_plane]


V

VeblenYoungProjectiveSpace [in ProjectiveGeometry.Space.projective_space_axioms]



Variable Index

D

DesarguesxD.desargues_theorem.A [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.alpha [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.A' [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.B [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.beta [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.B' [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.C [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.C' [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.gamma [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.O [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rAA' [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rAA'O [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rABC [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rABgamma [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rABO [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rACbeta [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rACO [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rA'B'C' [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rA'B'gamma [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rA'C'beta [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rBB' [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rBB'O [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rBCalpha [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rBCO [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rB'C'alpha [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rCC' [in ProjectiveGeometry.Space.desarguesxD]
DesarguesxD.desargues_theorem.rCC'O [in ProjectiveGeometry.Space.desarguesxD]
Desargues2Dfinal.desargues_theorem.A [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.alpha [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.A' [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.B [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.beta [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.B' [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.C [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.C' [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.gamma [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.O [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rAA' [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rAA'O [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rABC [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rABCA'B'C'O [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rABgamma [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rABO [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rACbeta [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rACO [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rA'B'C' [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rA'B'gamma [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rA'C'beta [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rA'O [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rBB' [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rBB'O [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rBCalpha [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rBCO [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rB'C'alpha [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rB'O [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rCC' [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rCC'O [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal.desargues_theorem.rC'O [in ProjectiveGeometry.Space.desargues2D]
Desargues2Dfinal2.desargues_theorem.A [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.alpha [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.A' [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.B [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.beta [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.B' [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.C [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.C' [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.gamma [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.O [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rAA' [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rAA'O [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rABC [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rABCA'B'C'O [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rABgamma [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rABO [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rACbeta [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rACO [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rA'B'C' [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rA'B'gamma [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rA'C'beta [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rBB' [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rBB'O [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rBCalpha [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rBCO [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rB'C'alpha [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rCC' [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dfinal2.desargues_theorem.rCC'O [in ProjectiveGeometry.Space.desargues2Dmore]
Desargues2Dlemmas2.desargues_plane.A [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.A' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.B [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.B' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.C [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.C' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.O [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.a_exists.a [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.a_exists.rka2 [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.a_exists.rka2' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.b_exists.b [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.b_exists.rkb2 [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.b_exists.rkb2' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.c_exists.c [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.c_exists.rkc2 [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.c_exists.rkc2' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.o [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.rko1 [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.rko2 [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.o_exists.rko3 [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.P [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.rABOP [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.P_exists.rOP [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rAA' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rAA'O [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rABC [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rABCA'B'C'O [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rABO [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rACO [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rA'B'C' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rA'B'O' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rA'C'O' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rBB' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rBB'O [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rBCO [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rB'C'O' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rCC' [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues2Dlemmas2.desargues_plane.rCC'O [in ProjectiveGeometry.Space.desargues2Dlemmas2]
Desargues3Dspecial.Desargues.A [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.a [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.alpha [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.B [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.b [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.beta [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.C [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.c [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.gamma [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.O [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.raAO [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rABC [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rabc [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rABCabc [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rabgamma [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rABgamma [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.racbeta [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rACbeta [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rbBO [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rbcalpha [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rBCalpha [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3Dspecial.Desargues.rcCO [in ProjectiveGeometry.Space.desargues3Dspecial]
Desargues3D.Desargues_general.a [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.A [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.alpha [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.b [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.B [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.beta [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.C [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.c [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.gamma [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.O [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.raA [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.raAO [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rABC [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rabc [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rABCabc [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rABgamma [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rabgamma [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rACbeta [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.racbeta [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rbB [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rbBO [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rbcalpha [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rBCalpha [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rcC [in ProjectiveGeometry.Space.desargues3D]
Desargues3D.Desargues_general.rcCO [in ProjectiveGeometry.Space.desargues3D]


F

fano_plane.A [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.ABF [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.ADG [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.B [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.BCD [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.BEG [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.C [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.CAE [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.CFG [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.D [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.DEF [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.E [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.F [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.G [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.Incid [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.Line [in ProjectiveGeometry.Plane.fano_plane_desargues]
fano_plane.Point [in ProjectiveGeometry.Plane.fano_plane_desargues]



Library Index

B

back
basic_facts
basic_facts_plane
bij


D

decidability
desarguesxD
desargues2D
desargues2Dlemmas
desargues2Dlemmas2
desargues2Dlemmas3
desargues2Dmore
desargues3D
desargues3Dlemmas
desargues3Dspecial


E

examples


F

fano_plane
fano_plane_desargues
field_variable_isolation_tactic
field_variable_isolation_tactic
flat
forth


G

general_tactics
general_tactics


H

hexamys
hexamys_desargues
Heyting_projective_plane_axioms
homogeneous


M

matroids_axioms
matroids_properties
matroid_to_matroid_p
moulton


P

pg25
projective_plane_axioms
projective_plane_duality
projective_plane_inst
projective_plane_to_Heyting_projective_plane
projective_space_axioms
projective_space_rank_axioms
projective_space_rank_to_projective_space
P05_almost_pappus
P06_angle_line
P07_cevian_lines
P08_cevian_lines_2
P09_complete_quadrilateral
P10_complete_quadrilateral_2
P11_chasles
P12_aeolian
P14_pseudo_midpoint


R

rank_properties


S

sets_of_points



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1185 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (426 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (11 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (87 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (9 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (159 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (153 entries)
Moduleid Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (102 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (188 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (50 entries)

This page has been generated by coqdoc