### Nuprl Lemma : least-equiv-cases

`∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].`
`  ∀a,b:A.`
`    ((least-equiv(A;R) a b)`
`    `` ((a = b ∈ A) ∨ ((R a b) ∨ (R b a)) ∨ (∃c:A. (((R c b) ∨ (R b c)) ∧ (least-equiv(A;R) a c)))))`

Proof

Definitions occuring in Statement :  least-equiv: `least-equiv(A;R)` uall: `∀[x:A]. B[x]` prop: `ℙ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` guard: `{T}` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` sym: `Sym(T;x,y.E[x; y])` least-equiv: `least-equiv(A;R)` transitive-reflexive-closure: `R^*` or: `P ∨ Q` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` so_apply: `x[s]` infix_ap: `x f y` exists: `∃x:A. B[x]` cand: `A c∧ B`
Lemmas referenced :  least-equiv-is-equiv least-equiv_wf or_wf exists_wf subtype_rel_self equal_wf transitive-closure-cases
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality applyEquality hypothesis functionEquality cumulativity universeEquality productElimination dependent_functionElimination independent_functionElimination sqequalRule unionElimination inlFormation equalitySymmetry lambdaEquality productEquality instantiate inrFormation dependent_pairFormation independent_pairFormation

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
\mforall{}a,b:A.
((least-equiv(A;R)  a  b)
{}\mRightarrow{}  ((a  =  b)  \mvee{}  ((R  a  b)  \mvee{}  (R  b  a))  \mvee{}  (\mexists{}c:A.  (((R  c  b)  \mvee{}  (R  b  c))  \mwedge{}  (least-equiv(A;R)  a  c)))))

Date html generated: 2018_05_21-PM-00_52_02
Last ObjectModification: 2018_05_04-AM-00_45_50

Theory : relations2

Home Index