optionEmbeddingEquiv — Mathlib

English

The preimage of a set under inl via sumSet equals the intersection with s.

Русский

Обратное изображение подмножества через inl относительно sumSet равно пересечению с s.

LaTeX

$$$.inl^{-1}(\\text{sumSet } h)^{-1}(r) = r \\cap s$$$

Lean4

/-- Equivalence between embeddings of `Option α` and a sigma type over the embeddings of `α`. -/
@[simps]
def optionEmbeddingEquiv (α β) : (Option α ↪ β) ≃ Σ f : α ↪ β, ↥(Set.range f)ᶜ
    where
  toFun f := ⟨Embedding.some.trans f, f none, fun ⟨x, hx⟩ ↦ Option.some_ne_none x <| f.injective hx⟩
  invFun f := f.1.optionElim f.2 f.2.2
  left_inv f := ext <| by rintro (_ | _) <;> simp
  right_inv := fun ⟨f, y, hy⟩ ↦ by ext <;> simp

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