ext — Mathlib

English

Two pre-sets x and y are equivalent iff they are mutually inclusive, i.e., x ⊆ y and y ⊆ x.

Русский

Два пред_mетства x и y эквивалентны тогда и только тогда, когда они включают друг друга: x ⊆ y и y ⊆ x.

LaTeX

$$$x\simeq y \iff (x\subseteq y) \land (y\subseteq x)$$$

Lean4

theorem ext : ∀ x y : PSet, Equiv x y ↔ x ⊆ y ∧ y ⊆ x
  | ⟨_, _⟩, ⟨_, _⟩ =>
    ⟨fun ⟨αβ, βα⟩ =>
      ⟨αβ, fun b =>
        let ⟨a, h⟩ := βα b
        ⟨a, Equiv.symm h⟩⟩,
      fun ⟨αβ, βα⟩ =>
      ⟨αβ, fun b =>
        let ⟨a, h⟩ := βα b
        ⟨a, Equiv.symm h⟩⟩⟩

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