bot_lie — Mathlib

English

Under suitable conditions, comap f of bracket [I,N₂] equals bracket I of comap f N₂.

Русский

При некоторых условиях прообраз по f скобки [I,N₂] равен скобке [I, прообраз f N₂].

LaTeX

$$$$ \operatorname{comap} f\,[I,N_2] = [I, \operatorname{comap} f N_2]. $$$$

Lean4

@[simp]
theorem bot_lie : ⁅(⊥ : LieIdeal R L), N⁆ = ⊥ :=
  by
  suffices ⁅(⊥ : LieIdeal R L), N⁆ ≤ ⊥ by exact le_bot_iff.mp this
  rw [lieIdeal_oper_eq_span, lieSpan_le]; rintro m ⟨⟨x, hx⟩, n, hn⟩; rw [← hn]
  change x ∈ (⊥ : LieIdeal R L) at hx; rw [mem_bot] at hx; simp [hx]

Похожие утверждения