lie_eq_bot_iff — Mathlib

English

A repetition of lie_coe_mem_lie expressing membership transfer through a bracket.

Русский

Повторение свойства lie_coe_mem_lie, показывающее перенос принадлежности через скобку.

LaTeX

$$$$ x \in I \land m \in N \Rightarrow \,[x,m] \in [I,N]. $$$$

Lean4

theorem lie_eq_bot_iff : ⁅I, N⁆ = ⊥ ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅(x : L), m⁆ = 0 :=
  by
  rw [lieIdeal_oper_eq_span, LieSubmodule.lieSpan_eq_bot_iff]
  refine ⟨fun h x hx m hm => h ⁅x, m⁆ ⟨⟨x, hx⟩, ⟨m, hm⟩, rfl⟩, ?_⟩
  rintro h - ⟨⟨x, hx⟩, ⟨⟨n, hn⟩, rfl⟩⟩
  exact h x hx n hn

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