New file

In this file...

Main declarations

• ConNF.foo: Something new.

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

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

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

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

The unordered pair.

Equations

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

@[simp]

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

def ConNF.TSet.op [Params] {α β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑β) (x y : TSet ↑γ) : 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 [Params] {α β : Λ} (hβ : ↑β < ↑α) {x y z w : TSet ↑β} (h : up hβ x y = up hβ z w) : x = z ∧ y = w ∨ x = w ∧ y = z

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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