nontrivial_iff_ne_bot — Mathlib

English

For any N, Nontrivial N is equivalent to N ≠ ⊥.

Русский

Для любого N: ненулевой эквивалентен N ≠ ⊥.

LaTeX

$$Nontrivial N \\iff N \\neq ⊥$$

Lean4

theorem nontrivial_iff_ne_bot {N : LieSubmodule R L M} : Nontrivial N ↔ N ≠ ⊥ :=
  by
  constructor <;> contrapose!
  · rintro rfl
    by_contra! h;
    rcases h with ⟨⟨m₁, h₁ : m₁ ∈ (⊥ : LieSubmodule R L M)⟩, ⟨m₂, h₂ : m₂ ∈ (⊥ : LieSubmodule R L M)⟩, h₁₂⟩
    simp [(LieSubmodule.mem_bot _).mp h₁, (LieSubmodule.mem_bot _).mp h₂] at h₁₂
  · rw [LieSubmodule.eq_bot_iff]
    rintro ⟨h⟩ m hm
    simpa using h ⟨m, hm⟩ ⟨_, N.zero_mem⟩

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