Rectangle

📁 Source: PrimeNumberTheoremAnd/Rectangle.lean

Statistics

Metric	Count
Definitions `RectangleBorder`, `Square`	2
Theorems `nhds_hasBasis_square`, `coe_toLinearEquiv_symm`, `RectSubRect`, `RectSubRect'`, `symm`, `symm_re`, `left_not_mem_uIoo`, `ne_left_of_mem_uIoo`, `ne_right_of_mem_uIoo`, `right_not_mem_uIoo`, `SmallSquareInRectangle`, `Square_apply`, `left_mem_rect`, `mapsTo_rectangleBorder_left_im`, `mapsTo_rectangleBorder_left_re`, `mapsTo_rectangleBorder_right_im`, `mapsTo_rectangleBorder_right_re`, `mapsTo_rectangle_left_im`, `mapsTo_rectangle_left_im_NoP`, `mapsTo_rectangle_left_re`, `mapsTo_rectangle_left_re_NoP`, `mapsTo_rectangle_right_im`, `mapsTo_rectangle_right_im_NoP`, `mapsTo_rectangle_right_re`, `mapsTo_rectangle_right_re_NoP`, `mem_Rect`, `not_mem_rectangleBorder_of_rectangle_mem_nhds`, `preimage_equivRealProdCLM_reProdIm`, `rect_subset_iff`, `rectangleBorder_disjoint_singleton`, `rectangleBorder_subset_punctured_rect`, `rectangleBorder_subset_rectangle`, `rectangle_disjoint_singleton`, `rectangle_in_convex`, `rectangle_mem_nhds_iff`, `rectangle_subset_punctured_rect`, `right_mem_rect`, `segment_reProdIm_segment_eq_convexHull`, `square_mem_nhds`, `square_neg`, `square_subset_square`	41
Total	43

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhds_hasBasis_square` 📖	mathematical	—	`Square`	—	—

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toLinearEquiv_symm` 📖	—	—	—	—	—

Rectangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`symm` 📖	—	—	—	—	—
`symm_re` 📖	—	—	—	—	—

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`left_not_mem_uIoo` 📖	—	—	—	—	—
`ne_left_of_mem_uIoo` 📖	—	—	—	—	`left_not_mem_uIoo`
`ne_right_of_mem_uIoo` 📖	—	—	—	—	`right_not_mem_uIoo`
`right_not_mem_uIoo` 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
`RectangleBorder` 📖	CompOp	9 math math: `mapsTo_rectangleBorder_right_re`, `mapsTo_rectangleBorder_right_im`, `rectangleBorder_subset_rectangle`, `mapsTo_rectangleBorder_left_im`, `mapsTo_rectangleBorder_left_re`, `rectangleBorder_disjoint_singleton`, `not_mem_rectangleBorder_of_rectangle_mem_nhds`, `MeromorphicOnRectangle.continuousOn`, `rectangleBorder_subset_punctured_rect`
`Square` 📖	CompOp	9 math math: `Square_apply`, `Perron.diffBddAtZero`, `square_subset_square`, `Perron.bddAbove_square_of_tendsto`, `SmallSquareInRectangle`, `square_neg`, `Perron.diffBddAtNegOne`, `Complex.nhds_hasBasis_square`, `square_mem_nhds`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`RectSubRect` 📖	—	—	—	—	`rect_subset_iff` `mem_Rect`
`RectSubRect'` 📖	—	—	—	—	`RectSubRect`
`SmallSquareInRectangle` 📖	mathematical	—	`Square`	—	`Complex.nhds_hasBasis_square` `square_subset_square`
`Square_apply` 📖	mathematical	—	`Square`	—	`Square.eq_1`
`left_mem_rect` 📖	—	—	—	—	—
`mapsTo_rectangleBorder_left_im` 📖	mathematical	—	`RectangleBorder`	—	—
`mapsTo_rectangleBorder_left_re` 📖	mathematical	—	`RectangleBorder`	—	—
`mapsTo_rectangleBorder_right_im` 📖	mathematical	—	`RectangleBorder`	—	—
`mapsTo_rectangleBorder_right_re` 📖	mathematical	—	`RectangleBorder`	—	—
`mapsTo_rectangle_left_im` 📖	—	—	—	—	—
`mapsTo_rectangle_left_im_NoP` 📖	—	`RectangleBorder`	—	—	`mapsTo_rectangleBorder_left_im` `rectangleBorder_subset_rectangle`
`mapsTo_rectangle_left_re` 📖	—	—	—	—	—
`mapsTo_rectangle_left_re_NoP` 📖	—	`RectangleBorder`	—	—	`mapsTo_rectangleBorder_left_re` `rectangleBorder_subset_rectangle`
`mapsTo_rectangle_right_im` 📖	—	—	—	—	—
`mapsTo_rectangle_right_im_NoP` 📖	—	`RectangleBorder`	—	—	`mapsTo_rectangleBorder_right_im` `rectangleBorder_subset_rectangle`
`mapsTo_rectangle_right_re` 📖	—	—	—	—	—
`mapsTo_rectangle_right_re_NoP` 📖	—	`RectangleBorder`	—	—	`mapsTo_rectangleBorder_right_re` `rectangleBorder_subset_rectangle`
`mem_Rect` 📖	—	—	—	—	—
`not_mem_rectangleBorder_of_rectangle_mem_nhds` 📖	mathematical	—	`RectangleBorder`	—	`rectangleBorder_disjoint_singleton` `rectangle_mem_nhds_iff` `Set.ne_left_of_mem_uIoo` `Set.ne_right_of_mem_uIoo`
`preimage_equivRealProdCLM_reProdIm` 📖	—	—	—	—	—
`rect_subset_iff` 📖	—	—	—	—	`left_mem_rect` `right_mem_rect`
`rectangleBorder_disjoint_singleton` 📖	mathematical	—	`RectangleBorder`	—	—
`rectangleBorder_subset_punctured_rect` 📖	mathematical	—	`RectangleBorder`	—	`rectangleBorder_subset_rectangle` `RectSubRect'` `rectangleBorder_disjoint_singleton`
`rectangleBorder_subset_rectangle` 📖	mathematical	—	`RectangleBorder`	—	—
`rectangle_disjoint_singleton` 📖	—	—	—	—	—
`rectangle_in_convex` 📖	—	—	—	—	`segment_reProdIm_segment_eq_convexHull`
`rectangle_mem_nhds_iff` 📖	—	—	—	—	—
`rectangle_subset_punctured_rect` 📖	—	—	—	—	`RectSubRect'` `rectangle_disjoint_singleton`
`right_mem_rect` 📖	—	—	—	—	—
`segment_reProdIm_segment_eq_convexHull` 📖	—	—	—	—	—
`square_mem_nhds` 📖	mathematical	—	`Square`	—	`Complex.nhds_hasBasis_square` `square_neg`
`square_neg` 📖	mathematical	—	`Square`	—	`Rectangle.symm`
`square_subset_square` 📖	mathematical	—	`Square`	—	`RectSubRect'`

---

← Back to Index