Skip to content

Commit 882a44f

Browse files
YaelDilliesYaelDillies
committed
delay imports
1 parent 55022e7 commit 882a44f

File tree

2 files changed

+62
-61
lines changed

2 files changed

+62
-61
lines changed

‎Mathlib/Order/Fin/Basic.lean

-61
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Robert Y. Lewis, Keeley Hoek
55
-/
66
import Mathlib.Data.Fin.Basic
7-
import Mathlib.Logic.Equiv.Fin
87
import Mathlib.Order.Hom.Set
98

109
#align_import data.fin.basic from "leanprover-community/mathlib"@"3a2b5524a138b5d0b818b858b516d4ac8a484b03"
@@ -340,63 +339,3 @@ lemma orderEmbedding_eq {f g : Fin n ↪o α} (h : range f = range g) : f = g :=
340339
#align fin.order_embedding_eq Fin.orderEmbedding_eq
341340

342341
end Fin
343-
344-
variable {n : ℕ}
345-
346-
/-- `Π i : Fin 2, α i` is order equivalent to `α 0 × α 1`. See also `OrderIso.finTwoArrowEquiv`
347-
for a non-dependent version. -/
348-
def OrderIso.piFinTwoIso (α : Fin 2 → Type*) [∀ i, Preorder (α i)] : (∀ i, α i) ≃o α 0 × α 1 where
349-
toEquiv := piFinTwoEquiv α
350-
map_rel_iff' := Iff.symm Fin.forall_fin_two
351-
#align order_iso.pi_fin_two_iso OrderIso.piFinTwoIso
352-
353-
/-- The space of functions `Fin 2 → α` is order equivalent to `α × α`. See also
354-
`OrderIso.piFinTwoIso`. -/
355-
def OrderIso.finTwoArrowIso (α : Type*) [Preorder α] : (Fin 2 → α) ≃o α × α :=
356-
{ OrderIso.piFinTwoIso fun _ => α with toEquiv := finTwoArrowEquiv α }
357-
#align order_iso.fin_two_arrow_iso OrderIso.finTwoArrowIso
358-
359-
/-- Order isomorphism between `Π j : Fin (n + 1), α j` and
360-
`α i × Π j : Fin n, α (Fin.succAbove i j)`. -/
361-
def OrderIso.piFinSuccAboveIso (α : Fin (n + 1) → Type*) [∀ i, LE (α i)]
362-
(i : Fin (n + 1)) : (∀ j, α j) ≃o α i × ∀ j, α (i.succAbove j) where
363-
toEquiv := Equiv.piFinSuccAbove α i
364-
map_rel_iff' := Iff.symm i.forall_iff_succAbove
365-
#align order_iso.pi_fin_succ_above_iso OrderIso.piFinSuccAboveIso
366-
367-
/-- `Fin.succAbove` as an order isomorphism between `Fin n` and `{x : Fin (n + 1) // x ≠ p}`. -/
368-
def finSuccAboveOrderIso (p : Fin (n + 1)) : Fin n ≃o { x : Fin (n + 1) // x ≠ p } where
369-
__ := finSuccAboveEquiv p
370-
map_rel_iff' := p.succAboveOrderEmb.map_rel_iff'
371-
#align fin_succ_above_equiv finSuccAboveOrderIso
372-
373-
lemma finSuccAboveOrderIso_apply (p : Fin (n + 1)) (i : Fin n) :
374-
finSuccAboveOrderIso p i = ⟨p.succAbove i, p.succAbove_ne i⟩ := rfl
375-
#align fin_succ_above_equiv_apply finSuccAboveOrderIso_apply
376-
377-
lemma finSuccAboveOrderIso_symm_apply_last (x : { x : Fin (n + 1) // x ≠ Fin.last n }) :
378-
(finSuccAboveOrderIso (Fin.last n)).symm x = Fin.castLT x.1 (Fin.val_lt_last x.2) := by
379-
rw [← Option.some_inj]
380-
simpa [finSuccAboveOrderIso, finSuccAboveEquiv, OrderIso.symm]
381-
using finSuccEquiv'_last_apply x.property
382-
#align fin_succ_above_equiv_symm_apply_last finSuccAboveEquiv_symm_apply_last
383-
384-
lemma finSuccAboveOrderIso_symm_apply_ne_last {p : Fin (n + 1)} (h : p ≠ Fin.last n)
385-
(x : { x : Fin (n + 1) // x ≠ p }) :
386-
(finSuccAboveEquiv p).symm x = (p.castLT (Fin.val_lt_last h)).predAbove x := by
387-
rw [← Option.some_inj]
388-
simpa [finSuccAboveEquiv, OrderIso.symm] using finSuccEquiv'_ne_last_apply h x.property
389-
#align fin_succ_above_equiv_symm_apply_ne_last finSuccAboveEquiv_symm_apply_ne_last
390-
391-
/-- Promote a `Fin n` into a larger `Fin m`, as a subtype where the underlying
392-
values are retained. This is the `OrderIso` version of `Fin.castLE`. -/
393-
@[simps apply symm_apply]
394-
def Fin.castLEOrderIso {n m : ℕ} (h : n ≤ m) : Fin n ≃o { i : Fin m // (i : ℕ) < n } where
395-
toFun i := ⟨Fin.castLE h i, by simp⟩
396-
invFun i := ⟨i, i.prop⟩
397-
left_inv _ := by simp
398-
right_inv _ := by simp
399-
map_rel_iff' := by simp [(strictMono_castLE h).le_iff_le]
400-
#align fin.cast_le_order_iso Fin.castLEOrderIso
401-
#align fin.cast_le_order_iso_apply Fin.castLEOrderIso_apply
402-
#align fin.cast_le_order_iso_symm_apply Fin.castLEOrderIso_symm_apply

‎Mathlib/Order/Fin/Tuple.lean

+62
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Floris van Doorn, Yury Kudryashov, Sébastien Gouëzel, Chris Hughes
55
-/
66
import Mathlib.Data.Fin.VecNotation
7+
import Mathlib.Logic.Equiv.Fin
78
import Mathlib.Order.Fin.Basic
89
import Mathlib.Order.Interval.Set.Basic
910
import Mathlib.Order.PiLex
@@ -111,3 +112,64 @@ lemma Antitone.vecCons (hf : Antitone f) (ha : f 0 ≤ a) : Antitone (vecCons a
111112
#align antitone.vec_cons Antitone.vecCons
112113

113114
example : Monotone ![1, 2, 2, 3] := by decide
115+
116+
117+
variable {n : ℕ}
118+
119+
/-- `Π i : Fin 2, α i` is order equivalent to `α 0 × α 1`. See also `OrderIso.finTwoArrowEquiv`
120+
for a non-dependent version. -/
121+
def OrderIso.piFinTwoIso (α : Fin 2 → Type*) [∀ i, Preorder (α i)] : (∀ i, α i) ≃o α 0 × α 1 where
122+
toEquiv := piFinTwoEquiv α
123+
map_rel_iff' := Iff.symm Fin.forall_fin_two
124+
#align order_iso.pi_fin_two_iso OrderIso.piFinTwoIso
125+
126+
/-- The space of functions `Fin 2 → α` is order equivalent to `α × α`. See also
127+
`OrderIso.piFinTwoIso`. -/
128+
def OrderIso.finTwoArrowIso (α : Type*) [Preorder α] : (Fin 2 → α) ≃o α × α :=
129+
{ OrderIso.piFinTwoIso fun _ => α with toEquiv := finTwoArrowEquiv α }
130+
#align order_iso.fin_two_arrow_iso OrderIso.finTwoArrowIso
131+
132+
/-- Order isomorphism between `Π j : Fin (n + 1), α j` and
133+
`α i × Π j : Fin n, α (Fin.succAbove i j)`. -/
134+
def OrderIso.piFinSuccAboveIso (α : Fin (n + 1) → Type*) [∀ i, LE (α i)]
135+
(i : Fin (n + 1)) : (∀ j, α j) ≃o α i × ∀ j, α (i.succAbove j) where
136+
toEquiv := Equiv.piFinSuccAbove α i
137+
map_rel_iff' := Iff.symm i.forall_iff_succAbove
138+
#align order_iso.pi_fin_succ_above_iso OrderIso.piFinSuccAboveIso
139+
140+
/-- `Fin.succAbove` as an order isomorphism between `Fin n` and `{x : Fin (n + 1) // x ≠ p}`. -/
141+
def finSuccAboveOrderIso (p : Fin (n + 1)) : Fin n ≃o { x : Fin (n + 1) // x ≠ p } where
142+
__ := finSuccAboveEquiv p
143+
map_rel_iff' := p.succAboveOrderEmb.map_rel_iff'
144+
#align fin_succ_above_equiv finSuccAboveOrderIso
145+
146+
lemma finSuccAboveOrderIso_apply (p : Fin (n + 1)) (i : Fin n) :
147+
finSuccAboveOrderIso p i = ⟨p.succAbove i, p.succAbove_ne i⟩ := rfl
148+
#align fin_succ_above_equiv_apply finSuccAboveOrderIso_apply
149+
150+
lemma finSuccAboveOrderIso_symm_apply_last (x : { x : Fin (n + 1) // x ≠ Fin.last n }) :
151+
(finSuccAboveOrderIso (Fin.last n)).symm x = Fin.castLT x.1 (Fin.val_lt_last x.2) := by
152+
rw [← Option.some_inj]
153+
simpa [finSuccAboveOrderIso, finSuccAboveEquiv, OrderIso.symm]
154+
using finSuccEquiv'_last_apply x.property
155+
#align fin_succ_above_equiv_symm_apply_last finSuccAboveEquiv_symm_apply_last
156+
157+
lemma finSuccAboveOrderIso_symm_apply_ne_last {p : Fin (n + 1)} (h : p ≠ Fin.last n)
158+
(x : { x : Fin (n + 1) // x ≠ p }) :
159+
(finSuccAboveEquiv p).symm x = (p.castLT (Fin.val_lt_last h)).predAbove x := by
160+
rw [← Option.some_inj]
161+
simpa [finSuccAboveEquiv, OrderIso.symm] using finSuccEquiv'_ne_last_apply h x.property
162+
#align fin_succ_above_equiv_symm_apply_ne_last finSuccAboveEquiv_symm_apply_ne_last
163+
164+
/-- Promote a `Fin n` into a larger `Fin m`, as a subtype where the underlying
165+
values are retained. This is the `OrderIso` version of `Fin.castLE`. -/
166+
@[simps apply symm_apply]
167+
def Fin.castLEOrderIso {n m : ℕ} (h : n ≤ m) : Fin n ≃o { i : Fin m // (i : ℕ) < n } where
168+
toFun i := ⟨Fin.castLE h i, by simp⟩
169+
invFun i := ⟨i, i.prop⟩
170+
left_inv _ := by simp
171+
right_inv _ := by simp
172+
map_rel_iff' := by simp [(strictMono_castLE h).le_iff_le]
173+
#align fin.cast_le_order_iso Fin.castLEOrderIso
174+
#align fin.cast_le_order_iso_apply Fin.castLEOrderIso_apply
175+
#align fin.cast_le_order_iso_symm_apply Fin.castLEOrderIso_symm_apply

0 commit comments

Comments
 (0)