HOL html

Files Index

Theorems Index

O (theorems)

OLDNET
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
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_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_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_LEMMA
OPEN_INTERVAL_MIDPOINT
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_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_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_UNION
OPEN_IN_UNIONS
OPEN_LIFT
OPEN_MAPPING_THM
OPEN_MAP_FROM_COMPOSITION_INJECTIVE
OPEN_MAP_FROM_COMPOSITION_SURJECTIVE
OPEN_MAP_IMP_CLOSED_MAP
OPEN_MAP_IMP_QUOTIENT_MAP
OPEN_MEASURABLE_INNER_DIVISION
OPEN_NEGATIONS
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_PATH_COMPONENT
OPEN_PATH_CONNECTED_COMPONENT
OPEN_PCROSS
OPEN_PCROSS_EQ
OPEN_POSITIVE_MULTIPLES
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_UNION
OPEN_UNIONS
OPEN_UNION_COMPACT_SUBSETS
OPEN_UNIV
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_TRANSLATION_EQ
ORTHGOONAL_TRANSFORMATION_REFLECT_ALONG
ORTHOGONAL_0
ORTHOGONAL_ANY_CLOSEST_POINT
ORTHOGONAL_BASIS
ORTHOGONAL_BASIS_BASIS
ORTHOGONAL_BASIS_EXISTS
ORTHOGONAL_BASIS_SUBSPACE
ORTHOGONAL_CLAUSES
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_SPANNINGSET_SUBSPACE
ORTHOGONAL_SUBSPACE_DECOMP
ORTHOGONAL_SUBSPACE_DECOMP_EXISTS
ORTHOGONAL_SUBSPACE_DECOMP_UNIQUE
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_BETWEEN_ORTHOGONAL_SETS
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_SURJECTIVE
ORTHOGONAL_VECTOR_ANGLE
ORTHONORMAL_BASIS_EXPAND
ORTHONORMAL_BASIS_SUBSPACE
ORTHONORMAL_CROSS
ORTHONORMAL_EXTENSION
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_PERMUTE
OSTROWSKI_THEOREM
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
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
onorm
open_def
open_in
open_interval
open_real_interval
open_real_segment
open_segment
operative
opposite
orthogonal
orthogonal_matrix
orthogonal_transformation
orthonormal
oth
outer
outermorphism
outside