Equivalence

📁 Source: Mathlib/ModelTheory/Equivalence.lean

Statistics

Metric	Count
Definitions Iff, Imp, iffSetoid, «term_⇔[_]_», «term_⟹[_]_»	5
Theorems all_iff_not_ex_not, ex_iff_not_all_not, iff_all_liftAt, iff_not_not, imp_iff_not_sup, inf_iff_not_sup_not, inf_not_iff_bot, sup_iff_not_inf_not, sup_not_iff_top, iff_not_not, imp_iff_not_sup, inf_iff_not_sup_not, sup_iff_not_inf_not, all, ex, imp, instIsTransBoundedFormula, instReflBoundedFormula, instSymmBoundedFormula, models_sentence_iff, mp, mpr, not, realize_bd_iff, realize_iff, refl, trans, instIsTransBoundedFormula, instReflBoundedFormula, refl, trans, bot_imp, iff_iff_imp_and_imp, imp_antisymm, imp_inf, imp_inf_iff, imp_sup_left, imp_sup_right, imp_top, inf_imp_left, inf_imp_right, sup_imp, sup_imp_iff	43
Total	48

FirstOrder

Definitions

Name	Category	Theorems
«term_⇔[_]_» 📖	CompOp	—
«term_⟹[_]_» 📖	CompOp	—

FirstOrder.Language.BoundedFormula

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
all_iff_not_ex_not 📖	mathematical	—	FirstOrder.Language.Theory.Iff all not ex	—	—
ex_iff_not_all_not 📖	mathematical	—	FirstOrder.Language.Theory.Iff ex not all	—	—
iff_all_liftAt 📖	mathematical	—	FirstOrder.Language.Theory.Iff all liftAt	—	realize_iff realize_all_liftAt_one_self FirstOrder.Language.Theory.ModelType.nonempty'
iff_not_not 📖	mathematical	—	FirstOrder.Language.Theory.Iff not	—	—
imp_iff_not_sup 📖	mathematical	—	FirstOrder.Language.Theory.Iff imp FirstOrder.Language.BoundedFormula instMax not	—	—
inf_iff_not_sup_not 📖	mathematical	—	FirstOrder.Language.Theory.Iff FirstOrder.Language.BoundedFormula instMin not instMax	—	—
inf_not_iff_bot 📖	mathematical	—	FirstOrder.Language.Theory.Iff FirstOrder.Language.BoundedFormula instMin not Bot.bot instBot	—	—
sup_iff_not_inf_not 📖	mathematical	—	FirstOrder.Language.Theory.Iff FirstOrder.Language.BoundedFormula instMax not instMin	—	—
sup_not_iff_top 📖	mathematical	—	FirstOrder.Language.Theory.Iff FirstOrder.Language.BoundedFormula instMax not Top.top instTop	—	—

FirstOrder.Language.Formula

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_not_not 📖	mathematical	—	FirstOrder.Language.Theory.Iff not	—	FirstOrder.Language.BoundedFormula.iff_not_not
imp_iff_not_sup 📖	mathematical	—	FirstOrder.Language.Theory.Iff imp FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.instMax not	—	FirstOrder.Language.BoundedFormula.imp_iff_not_sup
inf_iff_not_sup_not 📖	mathematical	—	FirstOrder.Language.Theory.Iff FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.instMin not FirstOrder.Language.Formula FirstOrder.Language.BoundedFormula.instMax	—	FirstOrder.Language.BoundedFormula.inf_iff_not_sup_not
sup_iff_not_inf_not 📖	mathematical	—	FirstOrder.Language.Theory.Iff FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.instMax not FirstOrder.Language.Formula FirstOrder.Language.BoundedFormula.instMin	—	FirstOrder.Language.BoundedFormula.sup_iff_not_inf_not

FirstOrder.Language.Theory

Definitions

Name	Category	Theorems
Iff 📖	MathDef	20 math math: FirstOrder.Language.BoundedFormula.ex_iff_not_all_not, FirstOrder.Language.Formula.iff_not_not, FirstOrder.Language.BoundedFormula.iff_all_liftAt, Iff.instSymmBoundedFormula, Iff.instIsTransBoundedFormula, FirstOrder.Language.BoundedFormula.iff_toPrenex, FirstOrder.Language.Formula.inf_iff_not_sup_not, iff_iff_imp_and_imp, FirstOrder.Language.BoundedFormula.inf_not_iff_bot, FirstOrder.Language.BoundedFormula.iff_not_not, FirstOrder.Language.BoundedFormula.sup_not_iff_top, FirstOrder.Language.BoundedFormula.imp_iff_not_sup, FirstOrder.Language.BoundedFormula.all_iff_not_ex_not, FirstOrder.Language.BoundedFormula.inf_iff_not_sup_not, FirstOrder.Language.Formula.imp_iff_not_sup, FirstOrder.Language.BoundedFormula.sup_iff_not_inf_not, Iff.refl, FirstOrder.Language.Formula.sup_iff_not_inf_not, Iff.instReflBoundedFormula, imp_antisymm
Imp 📖	MathDef	14 math math: imp_sup_right, imp_inf_iff, imp_sup_left, bot_imp, Imp.refl, inf_imp_left, inf_imp_right, Iff.mpr, Imp.instIsTransBoundedFormula, Imp.instReflBoundedFormula, iff_iff_imp_and_imp, Iff.mp, imp_top, sup_imp_iff
iffSetoid 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_imp 📖	mathematical	—	Imp Bot.bot FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.instBot	—	—
iff_iff_imp_and_imp 📖	mathematical	—	Iff Imp	—	—
imp_antisymm 📖	mathematical	Imp	Iff	—	iff_iff_imp_and_imp
imp_inf 📖	mathematical	Imp	FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.instMin	—	—
imp_inf_iff 📖	mathematical	—	Imp FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.instMin	—	Imp.trans inf_imp_left inf_imp_right imp_inf
imp_sup_left 📖	mathematical	—	Imp FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.instMax	—	—
imp_sup_right 📖	mathematical	—	Imp FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.instMax	—	—
imp_top 📖	mathematical	—	Imp Top.top FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.instTop	—	—
inf_imp_left 📖	mathematical	—	Imp FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.instMin	—	—
inf_imp_right 📖	mathematical	—	Imp FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.instMin	—	—
sup_imp 📖	mathematical	Imp	FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.instMax	—	—
sup_imp_iff 📖	mathematical	—	Imp FirstOrder.Language.BoundedFormula FirstOrder.Language.BoundedFormula.instMax	—	Imp.trans imp_sup_left imp_sup_right sup_imp

FirstOrder.Language.Theory.Iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
all 📖	mathematical	FirstOrder.Language.Theory.Iff	FirstOrder.Language.BoundedFormula.all	—	realize_bd_iff FirstOrder.Language.Theory.ModelType.nonempty' FirstOrder.Language.Theory.ModelType.is_model
ex 📖	mathematical	FirstOrder.Language.Theory.Iff	FirstOrder.Language.BoundedFormula.ex	—	realize_bd_iff FirstOrder.Language.Theory.ModelType.nonempty' FirstOrder.Language.Theory.ModelType.is_model
imp 📖	mathematical	FirstOrder.Language.Theory.Iff	FirstOrder.Language.BoundedFormula.imp	—	realize_bd_iff FirstOrder.Language.Theory.ModelType.nonempty' FirstOrder.Language.Theory.ModelType.is_model
instIsTransBoundedFormula 📖	mathematical	—	IsTrans FirstOrder.Language.BoundedFormula FirstOrder.Language.Theory.Iff	—	trans
instReflBoundedFormula 📖	mathematical	—	FirstOrder.Language.BoundedFormula FirstOrder.Language.Theory.Iff	—	refl
instSymmBoundedFormula 📖	mathematical	—	FirstOrder.Language.BoundedFormula FirstOrder.Language.Theory.Iff	—	symm
models_sentence_iff 📖	mathematical	FirstOrder.Language.Theory.Iff	FirstOrder.Language.Sentence.Realize	—	realize_iff Empty.instIsEmpty
mp 📖	mathematical	FirstOrder.Language.Theory.Iff	FirstOrder.Language.Theory.Imp	—	FirstOrder.Language.Theory.iff_iff_imp_and_imp
mpr 📖	mathematical	FirstOrder.Language.Theory.Iff	FirstOrder.Language.Theory.Imp	—	FirstOrder.Language.Theory.iff_iff_imp_and_imp
not 📖	mathematical	FirstOrder.Language.Theory.Iff	FirstOrder.Language.BoundedFormula.not	—	realize_bd_iff FirstOrder.Language.Theory.ModelType.nonempty' FirstOrder.Language.Theory.ModelType.is_model
realize_bd_iff 📖	mathematical	FirstOrder.Language.Theory.Iff	FirstOrder.Language.BoundedFormula.Realize	—	FirstOrder.Language.BoundedFormula.realize_iff FirstOrder.Language.Theory.ModelsBoundedFormula.realize_boundedFormula
realize_iff 📖	mathematical	FirstOrder.Language.Theory.Iff	FirstOrder.Language.Formula.Realize	—	realize_bd_iff Fin.isEmpty'
refl 📖	mathematical	—	FirstOrder.Language.Theory.Iff	—	FirstOrder.Language.BoundedFormula.realize_iff
trans 📖	—	FirstOrder.Language.Theory.Iff	—	—	FirstOrder.Language.BoundedFormula.realize_iff

FirstOrder.Language.Theory.Imp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsTransBoundedFormula 📖	mathematical	—	IsTrans FirstOrder.Language.BoundedFormula FirstOrder.Language.Theory.Imp	—	trans
instReflBoundedFormula 📖	mathematical	—	FirstOrder.Language.BoundedFormula FirstOrder.Language.Theory.Imp	—	refl
refl 📖	mathematical	—	FirstOrder.Language.Theory.Imp	—	—
trans 📖	—	FirstOrder.Language.Theory.Imp	—	—	—

---

← Back to Index