insert_symm_apply_inl

Mathlib.Logic.Equiv.Set

URI: https://scilib.ai/kg/mathlib#Equiv.Set.insert_symm_apply_inl

← MathLib Explorer

English

The backward map of insert sends Sum.inl b to ⟨b, Or.inr b.2⟩.

Русский

Обратное отображение вставки отправляет Sum.inl b в ⟨b, Or.inr b.2⟩.

LaTeX

$$insert H).symm (Sum.inl b) = ⟨b, Or.inr b.2⟩$$

Lean4

@[simp]
theorem insert_symm_apply_inl {α} {s : Set.{u} α} [DecidablePred (· ∈ s)] {a : α} (H : a ∉ s) (b : s) :
    (Equiv.Set.insert H).symm (Sum.inl b) = ⟨b, Or.inr b.2⟩ :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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