HOL html

Files Index

Theorems Index

O (theorems)

OCTAHEDRON_CONGRUENT_EDGES
OCTAHEDRON_CONGRUENT_FACETS
OCTAHEDRON_EDGES
OCTAHEDRON_EDGES_PER_FACE
OCTAHEDRON_EDGES_PER_VERTEX
OCTAHEDRON_VERTICES
ODD
ODDEVEN_INDUCT
ODDPART_LE
ODD_ADD
ODD_CONS
ODD_DOUBLE
ODD_EVEN
ODD_EVEN_INDUCT_LEMMA
ODD_EXISTS
ODD_EXP
ODD_MOD
ODD_MOD_2
ODD_MULT
ODD_ODDPART
ODD_ODD_OF_DISTINCT
ODD_OF_DISTINCT
ODD_OF_DISTINCT_OF_ODD
ODD_PHI_EQ
ODD_POLY_DIFF
ODD_POW2_MINUS1
ODD_SQUARE
ODD_SQUARE_MOD4
ODD_SUB
ODD_VARIATION_POSITIVE_ROOT
OEP
OLDGERMAN_LEMMA
OLDNET
ON
ONE
ONE_ONE
ONORM
ONORM_COMPOSE
ONORM_CONST
ONORM_EQ_0
ONORM_I
ONORM_ID
ONORM_NEG
ONORM_NEG_LEMMA
ONORM_POS_LE
ONORM_POS_LT
ONORM_TRIANGLE
ONORM_TRIANGLE_LE
ONORM_TRIANGLE_LT
ONTO
ON_CLAUSES
ON_HOMOL
OPEN_AFFINITY
OPEN_ARG_GT
OPEN_ARG_LTT
OPEN_BALL
OPEN_BIJECTIVE_LINEAR_IMAGE_EQ
OPEN_CLOSED
OPEN_CLOSED_INTERVAL_1
OPEN_CLOSED_INTERVAL_CONVEX
OPEN_COMPONENTS
OPEN_CONNECTED_COMPONENT
OPEN_CONTAINS_BALL
OPEN_CONTAINS_BALL_EQ
OPEN_CONTAINS_CBALL
OPEN_CONTAINS_CBALL_EQ
OPEN_CONVEX_HULL
OPEN_COUNTABLE_LIMIT_ELEMENTARY
OPEN_DELETE
OPEN_DIFF
OPEN_DROPOUT_3
OPEN_EMPTY
OPEN_EXISTS
OPEN_EXISTS_IN
OPEN_GENERAL_COMPONENT
OPEN_HALFSPACE_COMPONENT_GT
OPEN_HALFSPACE_COMPONENT_LT
OPEN_HALFSPACE_GT
OPEN_HALFSPACE_IM_GT
OPEN_HALFSPACE_IM_LT
OPEN_HALFSPACE_LT
OPEN_HALFSPACE_RE_GT
OPEN_HALFSPACE_RE_LT
OPEN_IMP_ANR
OPEN_IMP_ENR
OPEN_IMP_INFINITE
OPEN_IMP_LOCALLY_COMPACT
OPEN_IMP_LOCALLY_CONNECTED
OPEN_IMP_LOCALLY_PATH_CONNECTED
OPEN_IN
OPEN_INSIDE
OPEN_INTER
OPEN_INTERIOR
OPEN_INTERS
OPEN_INTERVAL
OPEN_INTERVAL_EQ
OPEN_INTERVAL_LEFT
OPEN_INTERVAL_LEMMA
OPEN_INTERVAL_MIDPOINT
OPEN_INTERVAL_RIGHT
OPEN_INTER_CLOSURE_EQ_EMPTY
OPEN_INTER_CLOSURE_SUBSET
OPEN_IN_CLAUSES
OPEN_IN_CLOSED_IN
OPEN_IN_CLOSED_IN_EQ
OPEN_IN_COMPONENTS_LOCALLY_CONNECTED
OPEN_IN_CONNECTED_COMPONENT
OPEN_IN_CONNECTED_COMPONENTS
OPEN_IN_CONNECTED_COMPONENT_LOCALLY_CONNECTED
OPEN_IN_CONTAINS_BALL
OPEN_IN_CONTAINS_CBALL
OPEN_IN_DELETE
OPEN_IN_DIFF
OPEN_IN_EMPTY
OPEN_IN_IMP_SUBSET
OPEN_IN_INJECTIVE_LINEAR_IMAGE
OPEN_IN_INTER
OPEN_IN_INTERS
OPEN_IN_INTER_OPEN
OPEN_IN_LOCALLY_COMPACT
OPEN_IN_OPEN
OPEN_IN_OPEN_EQ
OPEN_IN_OPEN_INTER
OPEN_IN_OPEN_TRANS
OPEN_IN_PATH_COMPONENT_LOCALLY_PATH_CONNECTED
OPEN_IN_PCROSS
OPEN_IN_PCROSS_EQ
OPEN_IN_REFL
OPEN_IN_RELATIVE_INTERIOR
OPEN_IN_SET_RELATIVE_INTERIOR
OPEN_IN_SING
OPEN_IN_SUBOPEN
OPEN_IN_SUBSET
OPEN_IN_SUBSET_RELATIVE_INTERIOR
OPEN_IN_SUBSET_TRANS
OPEN_IN_SUBTOPOLOGY
OPEN_IN_SUBTOPOLOGY_EMPTY
OPEN_IN_SUBTOPOLOGY_INTER_SUBSET
OPEN_IN_SUBTOPOLOGY_REFL
OPEN_IN_SUBTOPOLOGY_UNION
OPEN_IN_TOPSPACE
OPEN_IN_TRANS
OPEN_IN_TRANSLATION_EQ
OPEN_IN_TRANS_EQ
OPEN_IN_UNION
OPEN_IN_UNIONS
OPEN_LIFT
OPEN_MAPPING_THM
OPEN_MAP_CLOSED_SUPERSET_PREIMAGE
OPEN_MAP_CLOSED_SUPERSET_PREIMAGE_EQ
OPEN_MAP_FROM_COMPOSITION_INJECTIVE
OPEN_MAP_FROM_COMPOSITION_SURJECTIVE
OPEN_MAP_IFF_LOWER_HEMICONTINUOUS_PREIMAGE
OPEN_MAP_IMP_CLOSED_MAP
OPEN_MAP_IMP_QUOTIENT_MAP
OPEN_MAP_RESTRICT
OPEN_MEASURABLE_INNER_DIVISION
OPEN_NEGATIONS
OPEN_NEIGH
OPEN_NON_GENERAL_COMPONENT
OPEN_NON_PATH_COMPONENT
OPEN_NOT_NEGLIGIBLE
OPEN_OPEN_IN_TRANS
OPEN_OPEN_LEFT_PROJECTION
OPEN_OPEN_RIGHT_PROJECTION
OPEN_OUTSIDE
OPEN_OWN_NEIGH
OPEN_PATH_COMPONENT
OPEN_PATH_CONNECTED_COMPONENT
OPEN_PCROSS
OPEN_PCROSS_EQ
OPEN_POSITIVE_MULTIPLES
OPEN_POSITIVE_ORTHANT
OPEN_RCONE_GT
OPEN_SCALING
OPEN_SEGMENT_1
OPEN_SEGMENT_ALT
OPEN_SEGMENT_LINEAR_IMAGE
OPEN_SET_COCOUNTABLE_COORDINATES
OPEN_SET_COSMALL_COORDINATES
OPEN_SET_IRRATIONAL_COORDINATES
OPEN_SET_RATIONAL_COORDINATES
OPEN_SLICE
OPEN_SUBOPEN
OPEN_SUBSET
OPEN_SUBSET_INTERIOR
OPEN_SUMS
OPEN_SURJECTIVE_LINEAR_IMAGE
OPEN_TRANSLATION
OPEN_TRANSLATION_EQ
OPEN_UNICOHERENT_UNIV
OPEN_UNION
OPEN_UNIONS
OPEN_UNION_COMPACT_SUBSETS
OPEN_UNIV
OPEN_UNOPEN
OPEN_WEDGE
OPEN_WINDING_NUMBER_LEVELSETS
OPERATIVE_1_LE
OPERATIVE_1_LT
OPERATIVE_APPROXIMABLE
OPERATIVE_CONTENT
OPERATIVE_DIVISION
OPERATIVE_DIVISION_AND
OPERATIVE_EMPTY
OPERATIVE_FUNCTION_ENDPOINT_DIFF
OPERATIVE_INTEGRABLE
OPERATIVE_INTEGRAL
OPERATIVE_LIFTED_SETVARIATION
OPERATIVE_LIFTED_VECTOR_VARIATION
OPERATIVE_REAL_FUNCTION_ENDPOINT_DIFF
OPERATIVE_TAGGED_DIVISION
OPERATIVE_TRIVIAL
OPPOSITE_LINEAR_IMAGE_EQ
OPPOSITE_SIGNS
OPPOSITE_TRANSLATION_EQ
OR
ORDER
ORDERED_APPEND
ORDERED_CONS
ORDERED_QSORT
ORDER_1
ORDER_CONG
ORDER_DECOMP
ORDER_DEGREE
ORDER_DIFF
ORDER_DIVIDES
ORDER_DIVIDES_EXPDIFF
ORDER_DIVIDES_PHI
ORDER_EQ_0
ORDER_EXISTENCE_CARD
ORDER_EXISTENCE_FINITE
ORDER_EXISTENCE_GEN
ORDER_EXISTENCE_ITER
ORDER_MINIMAL
ORDER_MUL
ORDER_POLY
ORDER_ROOT
ORDER_THM
ORDER_UNIQUE
ORDER_WORKS
ORDINAL_CHAINED
ORDINAL_CHAINED_LEMMA
ORDINAL_SUC
ORDINAL_UNION
ORDINAL_UNION_LEMMA
ORDINAL_UP
ORIENTED_AREA_COLLINEAR_CONG
ORS
ORTHGOONAL_TRANSFORMATION_REFLECT_ALONG
ORTHOGONAL_0
ORTHOGONAL_ANY_CLOSEST_POINT
ORTHOGONAL_BASIS
ORTHOGONAL_BASIS_BASIS
ORTHOGONAL_BASIS_EXISTS
ORTHOGONAL_BASIS_SUBSPACE
ORTHOGONAL_CLAUSES
ORTHOGONAL_COMBINE
ORTHOGONAL_CROSS
ORTHOGONAL_EXTENSION
ORTHOGONAL_EXTENSION_STRONG
ORTHOGONAL_LINEAR_IMAGE_EQ
ORTHOGONAL_LNEG
ORTHOGONAL_LVSUM
ORTHOGONAL_MATRIX
ORTHOGONAL_MATRIX_2
ORTHOGONAL_MATRIX_2_ALT
ORTHOGONAL_MATRIX_ALT
ORTHOGONAL_MATRIX_EXISTS_BASIS
ORTHOGONAL_MATRIX_ID
ORTHOGONAL_MATRIX_INV
ORTHOGONAL_MATRIX_MATRIX
ORTHOGONAL_MATRIX_MUL
ORTHOGONAL_MATRIX_ORTHOGONAL_EIGENVECTORS
ORTHOGONAL_MATRIX_ORTHONORMAL_COLUMNS
ORTHOGONAL_MATRIX_ORTHONORMAL_COLUMNS_INDEXED
ORTHOGONAL_MATRIX_ORTHONORMAL_COLUMNS_PAIRWISE
ORTHOGONAL_MATRIX_ORTHONORMAL_COLUMNS_SPAN
ORTHOGONAL_MATRIX_ORTHONORMAL_ROWS
ORTHOGONAL_MATRIX_ORTHONORMAL_ROWS_INDEXED
ORTHOGONAL_MATRIX_ORTHONORMAL_ROWS_PAIRWISE
ORTHOGONAL_MATRIX_ORTHONORMAL_ROWS_SPAN
ORTHOGONAL_MATRIX_TRANSFORMATION
ORTHOGONAL_MATRIX_TRANSP
ORTHOGONAL_MUL
ORTHOGONAL_NULLSPACE_ROWSPACE
ORTHOGONAL_REFL
ORTHOGONAL_RNEG
ORTHOGONAL_ROTATION_OR_ROTOINVERSION
ORTHOGONAL_RVSUM
ORTHOGONAL_SCALING
ORTHOGONAL_SIMP_CLAUSES
ORTHOGONAL_SPANNINGSET_SUBSPACE
ORTHOGONAL_SUBSPACE_DECOMP
ORTHOGONAL_SUBSPACE_DECOMP_EXISTS
ORTHOGONAL_SUBSPACE_DECOMP_UNIQUE
ORTHOGONAL_SUM_LEMMA
ORTHOGONAL_SYM
ORTHOGONAL_TO_ORTHOGONAL_2D
ORTHOGONAL_TO_SPAN
ORTHOGONAL_TO_SPANS_EQ
ORTHOGONAL_TO_SPAN_EQ
ORTHOGONAL_TO_SUBSPACE_EXISTS
ORTHOGONAL_TO_SUBSPACE_EXISTS_GEN
ORTHOGONAL_TO_VECTOR_EXISTS
ORTHOGONAL_TRANSFORMATION
ORTHOGONAL_TRANSFORMATION_BALL
ORTHOGONAL_TRANSFORMATION_BETWEEN_ORTHOGONAL_SETS
ORTHOGONAL_TRANSFORMATION_CBALL
ORTHOGONAL_TRANSFORMATION_COMPOSE
ORTHOGONAL_TRANSFORMATION_EXISTS
ORTHOGONAL_TRANSFORMATION_EXISTS_1
ORTHOGONAL_TRANSFORMATION_GENERATED_BY_REFLECTIONS
ORTHOGONAL_TRANSFORMATION_I
ORTHOGONAL_TRANSFORMATION_ID
ORTHOGONAL_TRANSFORMATION_INJECTIVE
ORTHOGONAL_TRANSFORMATION_INTO_SUBSPACE
ORTHOGONAL_TRANSFORMATION_INVERSE
ORTHOGONAL_TRANSFORMATION_INVERSE_o
ORTHOGONAL_TRANSFORMATION_ISOMETRY
ORTHOGONAL_TRANSFORMATION_LINEAR
ORTHOGONAL_TRANSFORMATION_LOWDIM_HORIZONTAL
ORTHOGONAL_TRANSFORMATION_MATRIX
ORTHOGONAL_TRANSFORMATION_ONTO_SUBSPACE
ORTHOGONAL_TRANSFORMATION_ORTHOGONAL_EIGENVECTORS
ORTHOGONAL_TRANSFORMATION_ROTATE2D
ORTHOGONAL_TRANSFORMATION_SPHERE
ORTHOGONAL_TRANSFORMATION_SURJECTIVE
ORTHOGONAL_VANGLE
ORTHOGONAL_VECTOR
ORTHOGONAL_VECTOR_ANGLE
ORTHONORMAL_BASIS_EXPAND
ORTHONORMAL_BASIS_SUBSPACE
ORTHONORMAL_CROSS
ORTHONORMAL_EXTENSION
ORTHONORMAL_FOURIER_PARTIAL_SUM_DIFF_SQUARED
ORTHONORMAL_IMP_DISTINCT
ORTHONORMAL_IMP_INDEPENDENT
ORTHONORMAL_IMP_INDEPENDENT_EXPLICIT
ORTHONORMAL_IMP_INDEPENDENT_EXPLICIT_0
ORTHONORMAL_IMP_NONZERO
ORTHONORMAL_IMP_SPANNING
ORTHONORMAL_LINEAR_IMAGE
ORTHONORMAL_OPTIMAL_PARTIAL_SUM
ORTHONORMAL_PARTIAL_SUM_DIFF
ORTHONORMAL_PERMUTE
ORTHONORMAL_SYSTEM_L2NORM
ORTHONORMAL_SYSTEM_TRIGONOMETRIC_SET
OR_AND_COMM_lemma
OR_AND_DISTR_lemma
OR_ASSOC_lemma
OR_CLAUSES
OR_COMM_AND_lemma
OR_COMM_OR_lemma
OR_COMM_lemma
OR_DUAL
OR_DUAL2
OR_DUAL3
OR_EXISTS_THM
OR_False_lemma
OR_IMPLY_WEAK_lemma
OR_IMPLY_lemma
OR_LE_N_def
OR_LT_N_def
OR_NOT_AND_lemma
OR_OR_COMM_lemma
OR_OR_lemma
OR_True_lemma
OSTROWSKI_THEOREM
OTHER_DERIV_LEMMA
OUTER
OUTERMORPHISM_MBASIS
OUTERMORPHISM_MBASIS_EMPTY
OUTER_ACI
OUTER_ASSOC
OUTER_MBASIS
OUTER_MBASIS_LSCALAR
OUTER_MBASIS_REFL
OUTER_MBASIS_RSCALAR
OUTER_MBASIS_SING
OUTER_MBASIS_SKEWSYM
OUTL
OUTR
OUTSIDE
OUTSIDE_BOUNDED_NONEMPTY
OUTSIDE_COMPACT_IN_OPEN
OUTSIDE_CONNECTED_COMPONENT_LE
OUTSIDE_CONNECTED_COMPONENT_LT
OUTSIDE_CONVEX
OUTSIDE_EMPTY
OUTSIDE_FRONTIER_EQ_COMPLEMENT_CLOSURE
OUTSIDE_FRONTIER_MISSES_CLOSURE
OUTSIDE_INSIDE
OUTSIDE_IN_COMPONENTS
OUTSIDE_LINEAR_IMAGE
OUTSIDE_MONO
OUTSIDE_NO_OVERLAP
OUTSIDE_SAME_COMPONENT
OUTSIDE_SUBSET_CONVEX
OUTSIDE_TRANSLATION
OUTSIDE_UNION_OUTSIDE_UNION
OVERALL_BOUND_LEMMA
OVERPOWER_LEMMA
Ordered_DEF
o_ASSOC
o_DEF
o_THM
odd_bounded
odd_bounded_subset
odd_of_distinct
oddpart
old_prove
old_prove_by_refinement
on
on_circle
oncircle_with_diagonal
one
one_Axiom
one_DEF
one_INDUCT
one_RECURSION
one_axiom
one_over_plus1
onorm
open_EMPTY
open_and_closed
open_ball_center
open_ball_dist
open_ball_empty
open_ball_inter
open_ball_intersect
open_ball_nbd
open_ball_neg_radius
open_ball_nest
open_ball_nonempty
open_ball_nonempty_center
open_ball_open
open_ball_path
open_ball_star
open_ball_sub_closed
open_ball_subset
open_ball_subspace
open_closed
open_def
open_half_plane2D_FLT
open_half_plane2D_FLT_convex
open_half_plane2D_FLT_open
open_half_plane2D_LTF
open_half_plane2D_LTF_convex
open_half_plane2D_LTF_open
open_half_plane2D_LTS
open_half_plane2D_LTS_convex
open_half_plane2D_LTS_open
open_half_plane2D_SLT
open_half_plane2D_SLT_convex
open_half_plane2D_SLT_open
open_half_space_convex
open_half_space_diff
open_half_space_euclid
open_half_space_open
open_half_space_scale
open_in
open_induced
open_inters
open_interval
open_nbd
open_real_interval
open_real_segment
open_segment
openball_convex
openball_mk_segment_end
operative
opposite
option_INDUCT,option_RECURSION
or_def
or_left
or_right
or_thm_nn
or_thm_p
or_thm_q
order
order_imp_psegment
order_imp_psegment_shift
order_lt_imp_psegment
ordinal
oriented_area
oriented_areaSymmetry
orthogonal
orthogonal_matrix
orthogonal_transformation
orthonormal
orthonormal_coefficient
orthonormal_system
oth
other_end_prop
outer
outer_segment_even
outermorphism
outside