inl_mem_disjSum — Mathlib

English

For every a, inl(a) belongs to s.disjSum t if and only if a belongs to s.

Русский

Для каждого a верно: inl(a) ∈ s.disjSum t тогда и только тогда, когда a ∈ s.

LaTeX

$$$ \\forall a, \\ inl(a) \\in s.disjSum t \\iff a \\in s $$$

Lean4

@[simp]
theorem inl_mem_disjSum : inl a ∈ s.disjSum t ↔ a ∈ s :=
  by
  rw [mem_disjSum, or_iff_left]
  · simp only [inl.injEq, exists_eq_right]
  rintro ⟨b, _, hb⟩
  exact inr_ne_inl hb

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