preimage_inr — Mathlib

English

Let s be a finite subset of α ⊕ β. The set of β-elements whose right-inclusion image lies in s is exactly the right projection s.toRight, i.e. { b ∈ β : inr(b) ∈ s } = s.toRight.

Русский

Пусть s — конечное множество в α ⊕ β. Множество таких элементов β, образы которых через правое включение inr попадают в s, совпадает с правым проекционным множеством s.toRight, то есть { b ∈ β : inr(b) ∈ s } = s.toRight.

LaTeX

$$$\{ b \in \beta : \operatorname{inr}(b) \in s \} = s^{\mathrm{toRight}}$$$

Lean4

@[simp]
theorem preimage_inr (s : Finset (α ⊕ β)) : s.preimage Sum.inr Sum.inr_injective.injOn = s.toRight := by ext x; simp

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