mem_singleton_set_smul — Mathlib

English

x ∈ {r} • N iff ∃ m ∈ N with x = r • m.

Русский

x ∈ {r} • N тогда и только тогда, когда ∃ m ∈ N: x = r • m.

LaTeX

$$$ x \in \{r\} \cdot N \iff \exists m \in N,\ x = r \cdot m $$$

Lean4

theorem mem_singleton_set_smul [SMulCommClass R S M] (r : S) (x : M) :
    x ∈ ({ r } : Set S) • N ↔ ∃ (m : M), m ∈ N ∧ x = r • m :=
  by
  fconstructor
  · intro hx
    induction x, hx using Submodule.set_smul_inductionOn with
    | smul₀ => aesop
    | @smul₁ t n mem h =>
      rcases h with ⟨n, hn, rfl⟩
      exact ⟨t • n, by aesop, smul_comm _ _ _⟩
    | add mem₁ mem₂ h₁ h₂ =>
      rcases h₁ with ⟨m₁, h₁, rfl⟩
      rcases h₂ with ⟨m₂, h₂, rfl⟩
      exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by simp⟩
    | zero => exact ⟨0, Submodule.zero_mem _, by simp⟩
  · aesop

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