embDomain_single — Mathlib

English

For an embedding f and a, embDomain f (single a m) = single (f a) m.

Русский

Для вложения f и элемента a, embDomain f (single a m) = single (f a) m.

LaTeX

$$embDomain f (single a m) = single (f a) m$$

Lean4

@[simp]
theorem embDomain_single (f : α ↪ β) (a : α) (m : M) : embDomain f (single a m) = single (f a) m := by
  classical
  ext b
  by_cases h : b ∈ Set.range f
  · rcases h with ⟨a', rfl⟩
    simp [single_apply]
  · simp only [embDomain_notin_range, h, single_apply, not_false_iff]
    rw [if_neg]
    rintro rfl
    simp at h

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