subtypeOrEquiv — Mathlib

English

There is an equivalence between {x | p x ∨ q x} and {x | p x} ⊕ {x | q x} when p and q are disjoint.

Русский

Существует эквиваленция между {x | p x ∨ q x} и {x | p x} ⊕ {x | q x}, когда p и q несовместны.

LaTeX

$$$\\{ x \\mid p x \\lor q x\\} \\simeq (\\{ x \\mid p x\\} \\oplus \\{ x \\mid q x\\})$$$

Lean4

/-- A subtype `{x // p x ∨ q x}` over a disjunction of `p q : α → Prop` is equivalent to a sum of
subtypes `{x // p x} ⊕ {x // q x}` such that `¬ p x` is sent to the right, when
`Disjoint p q`.

See also `Equiv.sumCompl`, for when `IsCompl p q`. -/
@[simps (attr := grind =) apply]
def subtypeOrEquiv (p q : α → Prop) [DecidablePred p] (h : Disjoint p q) :
    { x // p x ∨ q x } ≃ { x // p x } ⊕ { x // q x }
    where
  toFun := subtypeOrLeftEmbedding p q
  invFun :=
    Sum.elim (Subtype.impEmbedding _ _ fun x hx ↦ (Or.inl hx : p x ∨ q x))
      (Subtype.impEmbedding _ _ fun x hx ↦ (Or.inr hx : p x ∨ q x))
  left_inv x := by grind
  right_inv
    x := by
    cases x with
    | inl x => grind
    | inr x =>
      simp only [Sum.elim_inr]
      rw [subtypeOrLeftEmbedding_apply_right]
      · grind
      · suffices ¬p x by simpa
        intro hp
        simpa using h.le_bot x ⟨hp, x.prop⟩

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