congr_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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