-
Notifications
You must be signed in to change notification settings - Fork 259
/
Hom.lean
111 lines (81 loc) · 2.99 KB
/
Hom.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
/-
Copyright (c) 2022 Yaël Dillies, Sara Rousta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import Mathlib.Order.UpperLower.Basic
import Mathlib.Order.Hom.CompleteLattice
#align_import order.upper_lower.hom from "leanprover-community/mathlib"@"0a0ec35061ed9960bf0e7ffb0335f44447b58977"
/-!
# `UpperSet.Ici` etc as `Sup`/`sSup`/`Inf`/`sInf`-homomorphisms
In this file we define `UpperSet.iciSupHom` etc. These functions are `UpperSet.Ici` and
`LowerSet.Iic` bundled as `SupHom`s, `InfHom`s, `sSupHom`s, or `sInfHom`s.
-/
variable {α : Type*}
open OrderDual
namespace UpperSet
section SemilatticeSup
variable [SemilatticeSup α]
/-- `UpperSet.Ici` as a `SupHom`. -/
def iciSupHom : SupHom α (UpperSet α) :=
⟨Ici, Ici_sup⟩
#align upper_set.Ici_sup_hom UpperSet.iciSupHom
@[simp]
theorem coe_iciSupHom : (iciSupHom : α → UpperSet α) = Ici :=
rfl
#align upper_set.coe_Ici_sup_hom UpperSet.coe_iciSupHom
@[simp]
theorem iciSupHom_apply (a : α) : iciSupHom a = Ici a :=
rfl
#align upper_set.Ici_sup_hom_apply UpperSet.iciSupHom_apply
end SemilatticeSup
variable [CompleteLattice α]
/-- `UpperSet.Ici` as a `sSupHom`. -/
def icisSupHom : sSupHom α (UpperSet α) :=
⟨Ici, fun s => (Ici_sSup s).trans sSup_image.symm⟩
-- Porting note: `ₓ` because typeclass assumption changed
#align upper_set.Ici_Sup_hom UpperSet.icisSupHomₓ
@[simp]
theorem coe_icisSupHom : (icisSupHom : α → UpperSet α) = Ici :=
rfl
-- Porting note: `ₓ` because typeclass assumption changed
#align upper_set.coe_Ici_Sup_hom UpperSet.coe_icisSupHomₓ
@[simp]
theorem icisSupHom_apply (a : α) : icisSupHom a = Ici a :=
rfl
-- Porting note: `ₓ` because typeclass assumption changed
#align upper_set.Ici_Sup_hom_apply UpperSet.icisSupHom_applyₓ
end UpperSet
namespace LowerSet
section SemilatticeInf
variable [SemilatticeInf α]
/-- `LowerSet.Iic` as an `InfHom`. -/
def iicInfHom : InfHom α (LowerSet α) :=
⟨Iic, Iic_inf⟩
#align lower_set.Iic_inf_hom LowerSet.iicInfHom
@[simp]
theorem coe_iicInfHom : (iicInfHom : α → LowerSet α) = Iic :=
rfl
#align lower_set.coe_Iic_inf_hom LowerSet.coe_iicInfHom
@[simp]
theorem iicInfHom_apply (a : α) : iicInfHom a = Iic a :=
rfl
#align lower_set.Iic_inf_hom_apply LowerSet.iicInfHom_apply
end SemilatticeInf
variable [CompleteLattice α]
/-- `LowerSet.Iic` as an `sInfHom`. -/
def iicsInfHom : sInfHom α (LowerSet α) :=
⟨Iic, fun s => (Iic_sInf s).trans sInf_image.symm⟩
-- Porting note: `ₓ` because typeclass assumption changed
#align lower_set.Iic_Inf_hom LowerSet.iicsInfHomₓ
@[simp]
theorem coe_iicsInfHom : (iicsInfHom : α → LowerSet α) = Iic :=
rfl
-- Porting note: `ₓ` because typeclass assumption changed
#align lower_set.coe_Iic_Inf_hom LowerSet.coe_iicsInfHomₓ
@[simp]
theorem iicsInfHom_apply (a : α) : iicsInfHom a = Iic a :=
rfl
-- Porting note: `ₓ` because typeclass assumption changed
#align lower_set.Iic_Inf_hom_apply LowerSet.iicsInfHom_applyₓ
end LowerSet