Embeddings between ZF sets

This file defines embeddings between ZFSets as injective functions and establishes their basic properties: reflexivity, transitivity, and existence of embeddings between singletons and pairs.

def ZFSet.hasEmbedding (A B : ZFSet.{u_1}) : Prop

Equations

• (A ↪ᶻ B) = ∃ (f : ZFSet.{?u.1}) (hf : A.IsFunc B f), f.IsInjective hf

def ZFSet.«term_↪ᶻ_» : Lean.TrailingParserDescr

Equations

• ZFSet.«term_↪ᶻ_» = Lean.ParserDescr.trailingNode `ZFSet.«term_↪ᶻ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↪ᶻ ") (Lean.ParserDescr.cat `term 51))

def ZFSet.«term_↩ᶻ_» : Lean.TrailingParserDescr

Equations

• ZFSet.«term_↩ᶻ_» = Lean.ParserDescr.trailingNode `ZFSet.«term_↩ᶻ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↩ᶻ ") (Lean.ParserDescr.cat `term 51))

theorem ZFSet.embedding_symm {A B : ZFSet.{u_1}} : A ↪ᶻ B ↔ (fun (A B : ZFSet.{u_1}) => B ↪ᶻ A) B A

theorem ZFSet.embedding_singleton {x y : ZFSet.{u_1}} : {x} ↪ᶻ {y}

theorem ZFSet.embedding_pair (a b c d : ZFSet.{u_1}) (hab_cd : a = b ↔ c = d) : {a, b} ↪ᶻ {c, d}

theorem ZFSet.embedding_refl (A : ZFSet.{u_1}) : A ↪ᶻ A

theorem ZFSet.embedding_trans {A B C : ZFSet.{u_1}} (hAB : A ↪ᶻ B) (hBC : B ↪ᶻ C) : A ↪ᶻ C