HOL html
| Files 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 | _ |
| Theorems 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 | _ |
W (theorems)
WALLISWALLIS_0
WALLIS_1
WALLIS_ALT
WALLIS_BOUNDS
WALLIS_EVEN
WALLIS_LT
WALLIS_MONO
WALLIS_NZ
WALLIS_ODD
WALLIS_PARTS
WALLIS_PARTS'
WALLIS_QUOTIENT
WALLIS_QUOTIENT'
WALLIS_RATIO_BOUNDS
WCR
WEDGE
WEDGE_ALT
WEDGE_DEGENERATE
WEDGE_LINEAR_IMAGE
WEDGE_LUNE
WEDGE_LUNE_GE
WEDGE_LUNE_GT
WEDGE_SPECIAL_SCALE
WEDGE_TRANSLATION
WEIERSTRASS_L2_TRIGONOMETRIC_SET
WEIERSTRASS_L2_TRIG_POLYNOMIAL
WEIERSTRASS_TRIG_POLYNOMIAL
WELLFORMED_RADICALS
WELLTYPED
WELLTYPED_CLAUSES
WELLTYPED_LEMMA
WF
WFP_PART_INDUCT
WFP_WF
WF_DCHAIN
WF_EQ
WF_EREC
WF_FALSE
WF_FINITE
WF_IND
WF_INT_MEASURE
WF_INT_MEASURE_2
WF_LEX
WF_LEX_DEPENDENT
WF_MEASURE
WF_MEASURE_GEN
WF_POINTWISE
WF_REC
WF_REC_CASES
WF_REC_CASES'
WF_REC_INVARIANT
WF_REC_TAIL
WF_REC_TAIL_GENERAL
WF_REC_TAIL_GENERAL'
WF_REC_WF
WF_REC_num
WF_REFL
WF_SUBSET
WF_TC
WF_UREC
WF_UREC_WF
WF_num
WHEN_PAR
WHILE_FIX
WHILE_THM
WHL_SEQ
WILSON
WILSON_EQ
WILSON_IMP
WILSON_LEMMA
WINDING_NUMBER
WINDING_NUMBER_AHLFORS
WINDING_NUMBER_AHLFORS_FULL
WINDING_NUMBER_AHLFORS_LEMMA
WINDING_NUMBER_AROUND_INSIDE
WINDING_NUMBER_AS_CONTINUOUS_LOGARITHM
WINDING_NUMBER_BIG_MEETS
WINDING_NUMBER_CIRCLEPATH
WINDING_NUMBER_COMPOSE_CEXP
WINDING_NUMBER_CONSTANT
WINDING_NUMBER_EQ
WINDING_NUMBER_EQUAL
WINDING_NUMBER_EQ_1
WINDING_NUMBER_FROM_INNERPATH
WINDING_NUMBER_HOMOTOPIC_LOOPS
WINDING_NUMBER_HOMOTOPIC_LOOPS_EQ
WINDING_NUMBER_HOMOTOPIC_LOOPS_NULL_EQ
WINDING_NUMBER_HOMOTOPIC_PATHS
WINDING_NUMBER_HOMOTOPIC_PATHS_EQ
WINDING_NUMBER_HOMOTOPIC_PATHS_NULL_EQ
WINDING_NUMBER_HOMOTOPIC_PATHS_NULL_EXPLICIT_EQ
WINDING_NUMBER_IVT_ABS
WINDING_NUMBER_IVT_NEG
WINDING_NUMBER_IVT_POS
WINDING_NUMBER_JOIN
WINDING_NUMBER_JOIN_POS_COMBINED
WINDING_NUMBER_LE_HALF
WINDING_NUMBER_LINEPATH_POS_LT
WINDING_NUMBER_LOOPS_LINEAR_EQ
WINDING_NUMBER_LT_1
WINDING_NUMBER_LT_HALF
WINDING_NUMBER_LT_HALF_LINEPATH
WINDING_NUMBER_NEARBY_LOOPS_EQ
WINDING_NUMBER_NEARBY_PATHS_EQ
WINDING_NUMBER_NEGATEPATH
WINDING_NUMBER_OFFSET
WINDING_NUMBER_PARTCIRCLEPATH_POS_LT
WINDING_NUMBER_PATHS_LINEAR_EQ
WINDING_NUMBER_POS_LE
WINDING_NUMBER_POS_LT
WINDING_NUMBER_POS_LT_LEMMA
WINDING_NUMBER_POS_MEETS
WINDING_NUMBER_REVERSEPATH
WINDING_NUMBER_SHIFTPATH
WINDING_NUMBER_SPLIT_LINEPATH
WINDING_NUMBER_STRONG
WINDING_NUMBER_SUBPATH_COMBINE
WINDING_NUMBER_SUBPATH_CONTINUOUS
WINDING_NUMBER_TRIANGLE
WINDING_NUMBER_TRIVIAL
WINDING_NUMBER_UNIQUE
WINDING_NUMBER_UNIQUE_LOOP
WINDING_NUMBER_VALID_PATH
WINDING_NUMBER_ZERO_ATINFINITY
WINDING_NUMBER_ZERO_IN_OUTSIDE
WINDING_NUMBER_ZERO_OUTSIDE
WINDING_NUMBER_ZERO_POINT
WITHIN
WITHINREAL_UNIV
WITHIN_UNIV
WITHIN_WITHIN
WLOG_LE
WLOG_LINEAR_INJECTIVE_IMAGE
WLOG_LINEAR_INJECTIVE_IMAGE_2
WLOG_LINEAR_INJECTIVE_IMAGE_2_ALT
WLOG_LINEAR_INJECTIVE_IMAGE_ALT
WLOG_LT
WN
WN_TC
WO
WOSET
WOSET_FLEQ
WOSET_POSET
WOSET_TOTAL_LE
WOSET_TOTAL_LT
WOSET_TRANS_LE
WOSET_TRANS_LESS
WOSET_WELL_CONTRAPOS
WP_ABORT
WP_ASSERT
WP_ASSIGN
WP_CONJUNCTIVE
WP_DISJUNCTIVE
WP_DO
WP_IF
WP_ITE
WP_MONOTONIC
WP_SEQ
WP_SKIP
WP_TOTAL
WP_WHILE
w0
w3
w4
weak_lemma
wedge
wellformed
welltyped
wemma
while_def
winding_number
within
wlp
woset
wp
wth