mem_toRight

Mathlib.Data.Finset.Sum

URI: https://scilib.ai/kg/mathlib#Finset.mem_toRight

English

b ∈ u.toRight iff inr b ∈ u.

Русский

b принадлежит toRight(u) тогда и только если inr(b) принадлежит u.

LaTeX

$$$ b \in u.toRight \iff \mathrm{inr}(b) \in u $$$

Lean4

@[simp]
theorem mem_toRight : b ∈ u.toRight ↔ .inr b ∈ u := by simp [toRight]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru