congr_right — Mathlib

English

If x ≃ y, then for any w, w ∈ x ↔ w ∈ y.

Русский

Если x эквивалентно y, тогда для любого w верно w ∈ x ⇔ w ∈ y.

LaTeX

$$$\\\\forall {x y : PSet},\\\\ x\\\\simeq y \\\\rightarrow \\\\forall {w : PSet}, w\\\\in x \\\\leftrightarrow w\\\\in y$$$

Lean4

theorem congr_right : ∀ {x y : PSet.{u}}, Equiv x y → ∀ {w : PSet.{u}}, w ∈ x ↔ w ∈ y
  | ⟨_, _⟩, ⟨_, _⟩, ⟨αβ, βα⟩, _ =>
    ⟨fun ⟨a, ha⟩ =>
      let ⟨b, hb⟩ := αβ a
      ⟨b, ha.trans hb⟩,
      fun ⟨b, hb⟩ =>
      let ⟨a, ha⟩ := βα b
      ⟨a, hb.euc ha⟩⟩

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