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 | _ |
P (theorems)
PAIR_SETS_EQPASTECART_BOUNDARY_CONDITIONS_FOR_PLANE_WAVES
PASTECART_CVECTOR_ADD
PASTECART_CVECTOR_MUL
PASTECART_CVECTOR_ZERO
PASTECART_EQ_CVECTOR_ZERO
PASTECART_VECTOR_MAP
PASTECART_VECTOR_MAP2
PLANE_AS_SPAN
PLANE_DECOMP
PLANE_DECOMP_DOT
PLANE_DECOMP_DOT_NORMAL
PLANE_NON_EMPTY
PLANE_OF_INCIDENCE_LAW
PLANE_SING
PLANE_SPAN
PLANE_SPAN_DECOMPOS
PLANE_SUBSPACE
PLANE_WAVE_WITH_PHASE_SHIFT_AT_INTERFACE
PLANE_WAVE_WITH_PHASE_SHIFT_AT_PLANE
PROJECTION_ON_HYPERPLANE_DECOMPOS
PROJECTION_ON_HYPERPLANE_THM
PROJECTION_ON_HYPERPLANE_THM_LNEG
phase_shift_at_plane
plane_of_interface
plane_wave
projection_on_hyperplane