File tree Expand file tree Collapse file tree 1 file changed +4
-4
lines changed
Mathlib/Order/Interval/Finset Expand file tree Collapse file tree 1 file changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -683,16 +683,16 @@ instance OrderDual.instLocallyFiniteOrder : LocallyFiniteOrder αᵒᵈ where
683
683
finset_mem_Ioc _ _ _ := (mem_Ico (α := α)).trans and_comm
684
684
finset_mem_Ioo _ _ _ := (mem_Ioo (α := α)).trans and_comm
685
685
686
- lemma Icc_orderDual_def (a b : αᵒᵈ) :
686
+ lemma Finset. Icc_orderDual_def (a b : αᵒᵈ) :
687
687
Icc a b = (Icc (ofDual b) (ofDual a)).map toDual.toEmbedding := map_refl.symm
688
688
689
- lemma Ico_orderDual_def (a b : αᵒᵈ) :
689
+ lemma Finset. Ico_orderDual_def (a b : αᵒᵈ) :
690
690
Ico a b = (Ioc (ofDual b) (ofDual a)).map toDual.toEmbedding := map_refl.symm
691
691
692
- lemma Ioc_orderDual_def (a b : αᵒᵈ) :
692
+ lemma Finset. Ioc_orderDual_def (a b : αᵒᵈ) :
693
693
Ioc a b = (Ico (ofDual b) (ofDual a)).map toDual.toEmbedding := map_refl.symm
694
694
695
- lemma Ioo_orderDual_def (a b : αᵒᵈ) :
695
+ lemma Finset. Ioo_orderDual_def (a b : αᵒᵈ) :
696
696
Ioo a b = (Ioo (ofDual b) (ofDual a)).map toDual.toEmbedding := map_refl.symm
697
697
698
698
lemma Finset.Icc_toDual : Icc (toDual a) (toDual b) = (Icc b a).map toDual.toEmbedding :=
You can’t perform that action at this time.
0 commit comments