subtypeInsertEquivOption — Mathlib

English

An element belongs to insert x t precisely when it equals x or belongs to t.

Русский

Элемент принадлежит вставке x t тогда и только тогда, когда он равен x или принадлежит t.

LaTeX

$$$a \in \operatorname{insert} x t \iff (a = x) \lor (a \in t)$$$

Lean4

/-- Inserting an element to a set is equivalent to the option type. -/
def subtypeInsertEquivOption [DecidableEq α] {t : Set α} {x : α} (h : x ∉ t) :
    { i // i ∈ insert x t } ≃ Option { i // i ∈ t }
    where
  toFun y := if h : ↑y = x then none else some ⟨y, by grind⟩
  invFun y := (y.elim ⟨x, mem_insert _ _⟩) fun z => ⟨z, by grind⟩
  left_inv y := by grind
  right_inv := by rintro (_ | y) <;> grind

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