HOL html

Files Index

Theorems Index

O (theorems)

OAPVION1
OAPVION2
OAPVION3
OBHTHCD
OBSTRUCT_EQ
OBS_IMP_NOT_IN_VC
OBS_SYM
OBTUSE_ANGLE_PROJECTION
OCBICBY
OCT23
OCT24
OCTO23
OCTOR23
ODD_B0
ODD_SUC_F
ODD_SUC_T
ODD_ZERO
ODIGPXU
ODIGPXU_lemma
ODXLSTCv2
OEHDBEN
OEHDBEN_PRIME
OFGJQUS
OIQKKEP
OJEKOJF
OJEKOJF2
OLDNET_FAN
OMEGA_LIST
OMEGA_LIST_0_EXPLICIT
OMEGA_LIST_1_EXPLICIT
OMEGA_LIST_1_EXPLICIT_NEW
OMEGA_LIST_2_EXPLICIT
OMEGA_LIST_2_EXPLICIT_NEW
OMEGA_LIST_3_EXPLICIT
OMEGA_LIST_BISECTOR
OMEGA_LIST_IN_VORONOI_LIST
OMEGA_LIST_LEMMA
OMEGA_LIST_N
OMEGA_LIST_N_EQ
OMEGA_LIST_N_EQ_GEN
OMEGA_LIST_N_IN_CONVEX_HULL
OMEGA_LIST_N_IN_FACET
OMEGA_LIST_N_IN_VORONOI_LIST
OMEGA_LIST_N_IN_VORONOI_LIST_GEN
OMEGA_LIST_N_LEMMA
OMEGA_LIST_TRUNCATE_0
OMEGA_LIST_TRUNCATE_1
OMEGA_LIST_TRUNCATE_1_NEW1
OMEGA_LIST_TRUNCATE_1_NEW2
OMEGA_LIST_TRUNCATE_2
OMEGA_LIST_TRUNCATE_2_NEW1
OMEGA_LIST_UP_TO_2
ONORM
ONORM_COMPOSE
ONORM_CONST
ONORM_EQ_0
ONORM_NEG
ONORM_NEG_LEMMA
ONORM_POS_LE
ONORM_POS_LT
ONORM_TRIANGLE
ONORM_TRIANGLE_LE
ONORM_TRIANGLE_LT
OPEN_AFF_GT_1_3
OPEN_AFF_GT_3_1
OPEN_BALL_FAN
OPEN_BIS_LT
OPEN_CLOSED_FAN
OPEN_CONTAINS_BALL_FAN
OPEN_CONTAINS_CBALL_FAN
OPEN_DELETE_FAN
OPEN_DIFF_AFF_GE
OPEN_DIFF_FAN
OPEN_EMPTY_FAN
OPEN_INTERIOR_FAN
OPEN_INTERS_FAN
OPEN_INTER_FAN
OPEN_IN_CLOSED_IN
OPEN_IN_CLOSED_IN_EQ
OPEN_IN_DIFF
OPEN_IN_EMPTY
OPEN_IN_FAN
OPEN_IN_INTER
OPEN_IN_OPEN_FAN
OPEN_IN_OPEN_TRANS_FAN
OPEN_IN_REFL
OPEN_IN_SUBOPEN
OPEN_IN_SUBSET
OPEN_IN_TRANS_FAN
OPEN_IN_UNION
OPEN_IN_UNIONS
OPEN_LIFT_FAN
OPEN_RCONE_GT
OPEN_REAL_INTERVAL_SING
OPEN_RELA_AFF_GT
OPEN_SUBOPEN_FAN
OPEN_TOPOLOGICAL_COMPONENT_YFAN
OPEN_TOPOLOGICAL_COMPONENT_YFAN_INTER_BALL
OPEN_TRANSLATION_FAN
OPEN_UNIONS_FAN
OPEN_UNION_FAN
OPEN_UNIV_FAN
OPPOSITE_SIDES_IMP_INTER
OPP_FAN_SYM_0
OPP_IMAGE_E_EQ
OPP_IMAGE_E_EQ_NEG
OPP_IMAGE_F_EQ
OPP_IMAGE_F_EQ2
OPP_IMAGE_F_EQ2_NEG
OPP_IMAGE_F_EQ_NEG
OPP_IMAGE_V_EQ
OPP_IMAGE_V_EQ_NEG
OPP_IS_SCS
OPP_SUC_MOD
ORBITS_EQ_SET_EDGE_FAN
ORBITS_SIGMA_FAN
ORBITS_SUBSET_EDGE_FAN
ORBIT_EQ_LIST_ORBIT
ORBIT_MAP_2
ORBIT_MAP_3
ORBIT_MAP_CARD_POS
ORBIT_MAP_INJ
ORBIT_MAP_INV_2
ORBIT_MAP_INV_2_SET
ORBIT_MAP_INV_3
ORBIT_MAP_INV_3_SET
ORBIT_MAP_PAIR_SUM_lemma
ORBIT_MAP_RES
ORBIT_MAP_RES_LEMMA
ORBIT_MAP_TRANSLATION
ORBIT_SUBSET_LEMMA
ORD2_ORBIT_MAP
ORDER
ORDER_AZIM_SUM2Pi
ORDER_AZIM_SUM2Pi0
ORDER_AZIM_SUM2Pi_0
ORDER_COVER1_SY
ORDER_COVER2_SY
ORDER_POWER_SIGMA_FAN
ORD_PAIRS_E_VV
ORD_PAIRS_INJ_IMAGE
ORTHOGONAL_0
ORTHOGONAL_AFF_HULL_2_KY_LEMMA
ORTHOGONAL_BASIS
ORTHOGONAL_BASIS_BASIS
ORTHOGONAL_BASIS_EXISTS
ORTHOGONAL_BASIS_SUBSPACE
ORTHOGONAL_CLAUSES
ORTHOGONAL_CROSS_PRODUCT
ORTHOGONAL_EXTENSION
ORTHOGONAL_IMP_PITHAGOR
ORTHOGONAL_LINEAR_IMAGE_EQ
ORTHOGONAL_LNEG
ORTHOGONAL_MATRIX
ORTHOGONAL_MATRIX_2
ORTHOGONAL_MATRIX_2_ALT
ORTHOGONAL_MATRIX_EXISTS_BASIS
ORTHOGONAL_MATRIX_ID
ORTHOGONAL_MATRIX_MUL
ORTHOGONAL_MATRIX_ORTHONORMAL_COLUMNS
ORTHOGONAL_MATRIX_ORTHONORMAL_ROWS
ORTHOGONAL_MATRIX_TRANSP
ORTHOGONAL_NULLSPACE_ROWSPACE
ORTHOGONAL_REFL
ORTHOGONAL_RNEG
ORTHOGONAL_ROTATION_OR_ROTOINVERSION
ORTHOGONAL_SCALING
ORTHOGONAL_SPANNINGSET_SUBSPACE
ORTHOGONAL_SUBSPACE_DECOMP
ORTHOGONAL_SUBSPACE_DECOMP_EXISTS
ORTHOGONAL_SUBSPACE_DECOMP_UNIQUE
ORTHOGONAL_SYM
ORTHOGONAL_TO_AFFINE_HULL_EQ
ORTHOGONAL_TO_ALL_IMP_ZERO
ORTHOGONAL_TO_ORTHOGONAL_2D
ORTHOGONAL_TO_SPAN
ORTHOGONAL_TO_SPANS_EQ
ORTHOGONAL_TO_SPAN_EQ
ORTHOGONAL_TO_SPAN_EXISTS
ORTHOGONAL_TO_SUBSPACE_EXISTS
ORTHOGONAL_TO_SUBSPACE_EXISTS_GEN
ORTHOGONAL_TO_VECTOR_EXISTS
ORTHOGONAL_TRANSFORMATION
ORTHOGONAL_TRANSFORMATION_EXISTS
ORTHOGONAL_TRANSFORMATION_EXISTS_1
ORTHOGONAL_TRANSFORMATION_I
ORTHOGONAL_TRANSFORMATION_ID
ORTHOGONAL_TRANSFORMATION_INJECTIVE
ORTHOGONAL_TRANSFORMATION_INVERSE
ORTHOGONAL_TRANSFORMATION_INVERSE_o
ORTHOGONAL_TRANSFORMATION_ISOMETRY
ORTHOGONAL_TRANSFORMATION_LINEAR
ORTHOGONAL_TRANSFORMATION_LOWDIM_HORIZONTAL
ORTHOGONAL_TRANSFORMATION_MATRIX
ORTHOGONAL_TRANSFORMATION_SURJECTIVE
ORTHOGORNAL_UNITIZE
ORTHONORMAL_BASIS
ORTHONORMAL_BASIS_SUBSPACE
ORTHONORMAL_CYCLIC
ORTHONORMAL_IMP_DISTINCT
ORTHONORMAL_IMP_INDEPENDENT
ORTHONORMAL_IMP_NONZERO
ORTHONORMAL_IMP_SPANNING
ORTHONORMAL_NOT_COLLINEAR
ORTHO_IMP_NORM_CROSS_PRODUCT
ORTHO_SPHERICAL_AZIM
OR_EXISTS_THM
OTHER_CONVEX_CONDI
OTHER_LEMMA
OTHORGONAL_QUATER_FOR
OTHORGONAL_WITH_COS
OTMTOTJ1
OTMTOTJ2
OTMTOTJ3
OTMTOTJ4
OWZLKVY0
OWZLKVY1
OWZLKVY2
OWZLKVY3
OWZLKVY4
OXLZLEZ
OZQVSFF
o_funs
oapp
obind
obstruct
obstructed
ocancel
odflt
old_prove
old_prove_by_refinement
omap
one_edge_fan
one_step
one_step_contour
onorm
open_ball
open_collinear_fan
open_continuous_eps
open_def_fan
open_delete_fan
open_half_plane
open_half_space
open_in
open_interval_fan
open_is_not_zero_fan
open_nua_kg
open_subsetU
open_vector_angle_fan
open_voronoi
opposite
opposite_components
opposite_hypermap
opposite_hypermap_connected
opposite_hypermap_plain
opposite_hypermap_simple
opposite_no_double_joints
opposite_no_loops
opposite_nondegenerate
opposite_opposite_hypermap_eq_hypermap
opposite_path
opposite_path_alt
opposite_planar
opposite_sets_of_components
opposite_tame_12o
opposite_tame_13a
orbit
orbit_character
orbit_cyclic
orbit_map
orbit_one_point
orbit_reflect
orbit_single_lemma
orbit_subset
orbit_sym
orbit_trans
ord_pairs
order
order_permutation
orderg
orientation
origin_is_not_aff_gt_fan
origin_not_in_rcone_fan
origin_point_not1_in_convex_fan
origin_point_not_in_convex_fan
ortho0
orthogonal
orthogonal_matrix
orthogonal_transformation
orthonormal
orthonormal1
orthonormal_e1_e2_e3_fan
orthosimplex
oth
override
ox3q1h()
ox3q1h_merge
oxl6142