Skip to content

Commit 39ba55a

Browse files
committed
chore(Geometry/Manifold): rename two lemmas using mathlib3 names (#11929)
- range_half_space -> range_euclideanHalfSpace - range_quadrant -> range_euclideanQuadrant
1 parent 1c861a0 commit 39ba55a

File tree

1 file changed

+6
-4
lines changed

1 file changed

+6
-4
lines changed

Mathlib/Geometry/Manifold/Instances/Real.lean

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -88,15 +88,17 @@ theorem EuclideanHalfSpace.ext [Zero (Fin n)] (x y : EuclideanHalfSpace n)
8888
(h : x.1 = y.1) : x = y :=
8989
Subtype.eq h
9090

91-
theorem range_half_space (n : ℕ) [Zero (Fin n)] :
91+
theorem range_euclideanHalfSpace (n : ℕ) [Zero (Fin n)] :
9292
(range fun x : EuclideanHalfSpace n => x.val) = { y | 0 ≤ y 0 } :=
9393
Subtype.range_val
94-
#align range_half_space range_half_space
94+
#align range_half_space range_euclideanHalfSpace
95+
@[deprecated] alias range_half_space := range_euclideanHalfSpace -- 2024-04-05
9596

96-
theorem range_quadrant (n : ℕ) :
97+
theorem range_euclideanQuadrant (n : ℕ) :
9798
(range fun x : EuclideanQuadrant n => x.val) = { y | ∀ i : Fin n, 0 ≤ y i } :=
9899
Subtype.range_val
99-
#align range_quadrant range_quadrant
100+
#align range_quadrant range_euclideanQuadrant
101+
@[deprecated] alias range_quadrant := range_euclideanQuadrant -- 2024-04-05
100102

101103
end
102104

0 commit comments

Comments
 (0)