Grace/Bootstrap/OrderedPair.g17

Open in Workbench Download source

Imports

None

Declarations

Source

1-- Checked facts about the Kuratowski pair (x, y) and its bound 𝒫(𝒫(A ∪ B)).2-- Elaborated before the module graph, after Aliases and Nat.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 Passmore78theorem bootstrap.pair.cancel_left (a b c : Set)9  requires h : {a, b} = {a, c}10  shows b = c11proof12  have hb : b = a ∨ b = c by rw ← pair.membership; rw ← h; simp13  have hc : c = a ∨ c = b by rw ← pair.membership; rw h; simp14  rcases hb with hba | hbc15  . rcases hc with hca | hcb16    . cc17    . cc18  . exact hbc1920theorem bootstrap.orderedPair.first (a b c d : Set)21  requires h : (a, b) = (c, d)22  shows a = c23proof24  simp [orderedPair] at h25  have hC : pair(c, c) ∈ {pair(a, a), {a, b}} by rw h; simp26  simp [pair.membership] at hC27  have ha : a ∈ pair(c, c)28    rcases hC with hC | hC29    . simp [hC]30    . simp [hC]31  simp [pair.membership] at ha32  tauto3334theorem bootstrap.orderedPair.injective (a b c d : Set)35  requires h : (a, b) = (c, d)36  shows a = c ∧ b = d37proof38  have first := bootstrap.orderedPair.first at a, b, c, d with h39  rw first at h40  simp [orderedPair] at h41  have outer := bootstrap.pair.cancel_left at pair(c, c), {c, b}, {c, d} with h42  exact ⟨first, (bootstrap.pair.cancel_left at c, b, d with outer)⟩4344theorem bootstrap.orderedPair.bounded (x y A B : Set)45  requires hx : x ∈ A46  requires hy : y ∈ B47  shows (x, y) ∈ 𝒫(𝒫(A ∪ B))48proof49  apply powerset.membership.backward at (x, y), 𝒫(A ∪ B)50  intros z hz51  simp [orderedPair, pair.membership] at hz52  rcases hz with hz | hz53  . simp [hz, powerset.membership, bootstrap.union2.membership]54  . simp [hz, powerset.membership, bootstrap.union2.membership]55