inr_mem_disjSum — Mathlib

English

For every b, inr(b) belongs to s.disjSum t if and only if b belongs to t.

Русский

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

LaTeX

$$$ \\forall b, \\ inr(b) \\in s.disjSum t \\iff b \\in t $$$

Lean4

@[simp]
theorem inr_mem_disjSum : inr b ∈ s.disjSum t ↔ b ∈ t :=
  by
  rw [mem_disjSum, or_iff_right]
  · simp only [inr.injEq, exists_eq_right]
  rintro ⟨a, _, ha⟩
  exact inl_ne_inr ha

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