mem_congr — Mathlib

English

If s ~ʷ t, then for every a, a ∈ s ↔ a ∈ t.

Русский

Если s ~ʷ t, то для каждого a: a ∈ s ⇔ a ∈ t.

LaTeX

$$$\forall {s,t:\mathrm{WSeq}(\alpha)},\ s \sim_W t \rightarrow \forall a, a \in s \Leftrightarrow a \in t$$$

Lean4

theorem mem_congr {s t : WSeq α} (h : s ~ʷ t) (a) : a ∈ s ↔ a ∈ t :=
  suffices ∀ {s t : WSeq α}, s ~ʷ t → a ∈ s → a ∈ t from ⟨this h, this h.symm⟩
  fun {_ _} h as =>
  let ⟨_, hn⟩ := exists_get?_of_mem as
  get?_mem ((get?_congr h _ _).1 hn)

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