congr_left — Mathlib

English

Equivalence x ≃ y implies x ∈ w ↔ y ∈ w for any w.

Русский

Если x ≃ y, то для любого w выполняется x ∈ w ↔ y ∈ w.

LaTeX

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

Lean4

theorem congr_left : ∀ {x y : PSet.{u}}, Equiv x y → ∀ {w : PSet.{u}}, x ∈ w ↔ y ∈ w
  | _, _, h, ⟨_, _⟩ => ⟨fun ⟨a, ha⟩ => ⟨a, h.symm.trans ha⟩, fun ⟨a, ha⟩ => ⟨a, h.trans ha⟩⟩

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