congr_left — Mathlib

English

If x ≃ y, then for any z we have x ⊆ z iff y ⊆ z.

Русский

Если x эквивалентно y, то для любого z выполняется x ⊆ z ⇔ y ⊆ z.

LaTeX

$$$\\forall x,y,z:\\mathrm{PSet},\\ x\\simeq y\\rightarrow (x\\subseteq z \\leftrightarrow y\\subseteq z)$$$

Lean4

theorem congr_left : ∀ {x y z : PSet}, Equiv x y → (x ⊆ z ↔ y ⊆ z)
  | ⟨_, _⟩, ⟨_, _⟩, ⟨_, _⟩, ⟨αβ, βα⟩ =>
    ⟨fun αγ b =>
      let ⟨a, ba⟩ := βα b
      let ⟨c, ac⟩ := αγ a
      ⟨c, (Equiv.symm ba).trans ac⟩,
      fun βγ a =>
      let ⟨b, ab⟩ := αβ a
      let ⟨c, bc⟩ := βγ b
      ⟨c, Equiv.trans ab bc⟩⟩

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