mem_insert_iff — Mathlib

English

For all x,y,z, x is in insert y z iff x is equivalent to y or x is in z.

Русский

Для всех x,y,z: x ∈ insert(y,z) тогда и только тогда, когда x эквивалентно y или x ∈ z.

LaTeX

$$$$ x \in \operatorname{insert}(y,z) \iff \operatorname{Equiv}(x,y) \lor x \in z $$$$

Lean4

@[simp]
theorem mem_insert_iff : ∀ {x y z : PSet.{u}}, x ∈ insert y z ↔ Equiv x y ∨ x ∈ z
  | x, y, ⟨α, A⟩ =>
    show (x ∈ PSet.mk (Option α) fun o => Option.rec y A o) ↔ Equiv x y ∨ x ∈ PSet.mk α A from
      ⟨fun m =>
        match m with
        | ⟨some a, ha⟩ => Or.inr ⟨a, ha⟩
        | ⟨none, h⟩ => Or.inl h,
        fun m =>
        match m with
        | Or.inr ⟨a, ha⟩ => ⟨some a, ha⟩
        | Or.inl h => ⟨none, h⟩⟩

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