Theorems · Theorem · logic and foundations

Equiv.Set.union_apply_right

∀ {α : Type u_3} {s t : Set α} [inst : DecidablePred fun x => x ∈ s] (H : Disjoint s t) {a : ↑(s ∪ t)} (ha : ↑a ∈ t),
  (Equiv.Set.union H) a = Sum.inr ⟨↑a, ha⟩

Defined in

Mathlib.Logic.Equiv.Set

Cited by

2 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidablePred