R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
h : ∀ {N N' : LieSubmodule R L M}, ↑N ≤ ↑N' ↔ N ≤ N'
⊢ IsGLB S (sInf S)
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
⊢ IsGLB S (sInf S)
have h : ∀ {N N' : LieSubmodule R L M}, (N : Set M) ≤ N' ↔ N ≤ N' := fun {_ _} ↦ Iff.rfl
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
h : ∀ {N N' : LieSubmodule R L M}, ↑N ≤ ↑N' ↔ N ≤ N'
⊢ IsGLB ((fun {x} => ↑x) '' S) ↑(sInf S)
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
h : ∀ {N N' : LieSubmodule R L M}, ↑N ≤ ↑N' ↔ N ≤ N'
⊢ IsGLB S (sInf S)
apply IsGLB.of_image h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
h : ∀ {N N' : LieSubmodule R L M}, ↑N ≤ ↑N' ↔ N ≤ N'
⊢ IsGLB ((fun {x} => ↑x) '' S) (⋂ (s : LieSubmodule R L M) (_ : s ∈ S), ↑s)
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
h : ∀ {N N' : LieSubmodule R L M}, ↑N ≤ ↑N' ↔ N ≤ N'
⊢ IsGLB ((fun {x} => ↑x) '' S) ↑(sInf S)
simp only [sInf_coe]
no goals
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N N' : LieSubmodule R L M
I J : LieIdeal R L
S : Set (LieSubmodule R L M)
h : ∀ {N N' : LieSubmodule R L M}, ↑N ≤ ↑N' ↔ N ≤ N'
⊢ IsGLB ((fun {x} => ↑x) '' S) (⋂ (s : LieSubmodule R L M) (_ : s ∈ S), ↑s)
exact isGLB_biInf