R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
⊢ (⋂ (p : Submodule R L) (_ : p ∈ {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}), ↑p) = ⋂ (s : LieSubalgebra R L) (_ : s ∈ S), ↑s
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
⊢ ↑(sInf S) = ⋂ (s : LieSubalgebra R L) (_ : s ∈ S), ↑s
rw [← coe_to_submodule, sInf_coe_to_submodule, Submodule.sInf_coe]
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
x : L
⊢ (x ∈ ⋂ (p : Submodule R L) (_ : p ∈ {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}), ↑p) ↔
    x ∈ ⋂ (s : LieSubalgebra R L) (_ : s ∈ S), ↑s
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
⊢ (⋂ (p : Submodule R L) (_ : p ∈ {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}), ↑p) = ⋂ (s : LieSubalgebra R L) (_ : s ∈ S), ↑s
ext x
no goals
case h
R : Type u
L : Type v
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
L₂ : Type w
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L →ₗ⁅R⁆ L₂
K K' : LieSubalgebra R L
K₂ : LieSubalgebra R L₂
S : Set (LieSubalgebra R L)
x : L
⊢ (x ∈ ⋂ (p : Submodule R L) (_ : p ∈ {x | ∃ s, s ∈ S ∧ s.toSubmodule = x}), ↑p) ↔
    x ∈ ⋂ (s : LieSubalgebra R L) (_ : s ∈ S), ↑s
simp