Grace/Bootstrap/Epsilon0.g17

Open in Workbench Download source

Imports

None

Declarations

• epsilon0.less def
• epsilon0.less.membership theorem derivation

Source

1-- The membership order on ε₀, cut out of 𝒫(𝒫(ε₀ ∪ ε₀)) by Separation.2-- Elaborated before the module graph, after Aliases, Nat, and OrderedPair.3-- Part of the Grace17 proof assistant for mathematics based on set theory.4-- Copyright (c) 2026 Grant Olney Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78def epsilon0.less : Set :=9  { p ∈ 𝒫(𝒫(ε₀ ∪ ε₀)) | ∃ x ∈ ε₀, ∃ y ∈ ε₀, x ∈ y ∧ p = (x, y) }1011theorem epsilon0.less.membership (a b : Set)12  shows relates(ε₀.less, a, b) ↔ (a ∈ ε₀ ∧ b ∈ ε₀ ∧ a ∈ b)13proof14  constructor15  . intro h16    simp [relates, ε₀.less] at h17    obtain ⟨bound, x, hx, y, hy, hxy, pair⟩ := h18    obtain ⟨ha, hb⟩ := bootstrap.orderedPair.injective at a, b, x, y with pair19    rw [ha, hb]20    exact ⟨hx, hy, hxy⟩21  . intro h22    obtain ⟨ha, hb, hab⟩ := h23    have bound := bootstrap.orderedPair.bounded at a, b, ε₀, ε₀ with ha, hb24    simp [relates, ε₀.less]25