New file

In this file...

Main declarations

• ConNF.foo: Something new.

theorem ConNF.TSet.exists_inter [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) (x y : ConNF.TSet ↑α) : ∃ (w : ConNF.TSet ↑α), ∀ (z : ConNF.TSet ↑β), z ∈[hβ] w ↔ z ∈[hβ] x ∧ z ∈[hβ] y

theorem ConNF.TSet.exists_compl [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) (x : ConNF.TSet ↑α) : ∃ (y : ConNF.TSet ↑α), ∀ (z : ConNF.TSet ↑β), z ∈[hβ] y ↔ ¬z ∈[hβ] x

theorem ConNF.TSet.exists_up [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) (x y : ConNF.TSet ↑β) : ∃ (w : ConNF.TSet ↑α), ∀ (z : ConNF.TSet ↑β), z ∈[hβ] w ↔ z = x ∨ z = y

def ConNF.TSet.up [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) (x y : ConNF.TSet ↑β) : ConNF.TSet ↑α

The unordered pair.

Equations

• ConNF.TSet.up hβ x y = ⋯.choose

@[simp]

theorem ConNF.TSet.mem_up_iff [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) (x y z : ConNF.TSet ↑β) : z ∈[hβ] ConNF.TSet.up hβ x y ↔ z = x ∨ z = y

def ConNF.TSet.op [ConNF.Params] {α β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x y : ConNF.TSet ↑γ) : ConNF.TSet ↑α

The Kuratowski ordered pair.

Equations

• ConNF.TSet.op hβ hγ x y = ConNF.TSet.up hβ (ConNF.singleton hγ x) (ConNF.TSet.up hγ x y)

theorem ConNF.TSet.up_injective [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) {x y z w : ConNF.TSet ↑β} (h : ConNF.TSet.up hβ x y = ConNF.TSet.up hβ z w) : x = z ∧ y = w ∨ x = w ∧ y = z

@[simp]

theorem ConNF.TSet.up_inj [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) (x y z w : ConNF.TSet ↑β) : ConNF.TSet.up hβ x y = ConNF.TSet.up hβ z w ↔ x = z ∧ y = w ∨ x = w ∧ y = z

@[simp]

theorem ConNF.TSet.up_self [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) {x : ConNF.TSet ↑β} : ConNF.TSet.up hβ x x = ConNF.singleton hβ x

@[simp]

theorem ConNF.TSet.up_eq_singleton_iff [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) (x y z : ConNF.TSet ↑β) : ConNF.TSet.up hβ x y = ConNF.singleton hβ z ↔ x = z ∧ y = z

@[simp]

theorem ConNF.TSet.singleton_eq_up_iff [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) (x y z : ConNF.TSet ↑β) : ConNF.singleton hβ z = ConNF.TSet.up hβ x y ↔ x = z ∧ y = z

theorem ConNF.TSet.op_injective [ConNF.Params] {α β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) {x y z w : ConNF.TSet ↑γ} (h : ConNF.TSet.op hβ hγ x y = ConNF.TSet.op hβ hγ z w) : x = z ∧ y = w

@[simp]

theorem ConNF.TSet.op_inj [ConNF.Params] {α β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x y z w : ConNF.TSet ↑γ) : ConNF.TSet.op hβ hγ x y = ConNF.TSet.op hβ hγ z w ↔ x = z ∧ y = w

@[simp]

theorem ConNF.TSet.smul_up [ConNF.Params] {α β : ConNF.Λ} (hβ : ↑β < ↑α) (x y : ConNF.TSet ↑β) (ρ : ConNF.AllPerm ↑α) : ρ • ConNF.TSet.up hβ x y = ConNF.TSet.up hβ (ρ ↘ hβ • x) (ρ ↘ hβ • y)

@[simp]

theorem ConNF.TSet.smul_op [ConNF.Params] {α β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x y : ConNF.TSet ↑γ) (ρ : ConNF.AllPerm ↑α) : ρ • ConNF.TSet.op hβ hγ x y = ConNF.TSet.op hβ hγ (ρ ↘ hβ ↘ hγ • x) (ρ ↘ hβ ↘ hγ • y)

theorem ConNF.TSet.exists_singletonImage [ConNF.Params] {α β γ δ ε : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (x : ConNF.TSet ↑β) : ∃ (y : ConNF.TSet ↑α), ∀ (z w : ConNF.TSet ↑ε), ConNF.TSet.op hγ hδ (ConNF.singleton hε z) (ConNF.singleton hε w) ∈[hβ] y ↔ ConNF.TSet.op hδ hε z w ∈[hγ] x

theorem ConNF.TSet.exists_insertion2 [ConNF.Params] {α β γ δ ε ζ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (hζ : ↑ζ < ↑ε) (x : ConNF.TSet ↑γ) : ∃ (y : ConNF.TSet ↑α), ∀ (a b c : ConNF.TSet ↑ζ), ConNF.TSet.op hγ hδ (ConNF.singleton hε (ConNF.singleton hζ a)) (ConNF.TSet.op hε hζ b c) ∈[hβ] y ↔ ConNF.TSet.op hε hζ a c ∈[hδ] x

theorem ConNF.TSet.exists_insertion3 [ConNF.Params] {α β γ δ ε ζ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (hζ : ↑ζ < ↑ε) (x : ConNF.TSet ↑γ) : ∃ (y : ConNF.TSet ↑α), ∀ (a b c : ConNF.TSet ↑ζ), ConNF.TSet.op hγ hδ (ConNF.singleton hε (ConNF.singleton hζ a)) (ConNF.TSet.op hε hζ b c) ∈[hβ] y ↔ ConNF.TSet.op hε hζ a b ∈[hδ] x

theorem ConNF.TSet.exists_cross [ConNF.Params] {α β γ δ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (x : ConNF.TSet ↑γ) : ∃ (y : ConNF.TSet ↑α), ∀ (a : ConNF.TSet ↑β), a ∈[hβ] y ↔ ∃ (b : ConNF.TSet ↑δ) (c : ConNF.TSet ↑δ), a = ConNF.TSet.op hγ hδ b c ∧ c ∈[hδ] x

theorem ConNF.TSet.exists_typeLower [ConNF.Params] {α β γ δ ε : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) (x : ConNF.TSet ↑α) : ∃ (y : ConNF.TSet ↑δ), ∀ (a : ConNF.TSet ↑ε), a ∈[hε] y ↔ ∀ (b : ConNF.TSet ↑δ), ConNF.TSet.op hγ hδ b (ConNF.singleton hε a) ∈[hβ] x

theorem ConNF.TSet.exists_converse [ConNF.Params] {α β γ δ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (x : ConNF.TSet ↑α) : ∃ (y : ConNF.TSet ↑α), ∀ (a b : ConNF.TSet ↑δ), ConNF.TSet.op hγ hδ a b ∈[hβ] y ↔ ConNF.TSet.op hγ hδ b a ∈[hβ] x

theorem ConNF.TSet.exists_cardinalOne [ConNF.Params] {α β γ : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) : ∃ (x : ConNF.TSet ↑α), ∀ (a : ConNF.TSet ↑β), a ∈[hβ] x ↔ ∃ (b : ConNF.TSet ↑γ), ∀ (c : ConNF.TSet ↑γ), c ∈[hγ] a ↔ c = b

theorem ConNF.TSet.exists_subset [ConNF.Params] {α β γ δ ε : ConNF.Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑δ) : ∃ (x : ConNF.TSet ↑α), ∀ (a b : ConNF.TSet ↑δ), ConNF.TSet.op hγ hδ a b ∈[hβ] x ↔ ∀ (c : ConNF.TSet ↑ε), c ∈[hε] a → c ∈[hε] b