Plain-language statement
Blueprint Lemma 13.2(v). E255 at x ↔ L_x ∘ R_x has a fixed point.
Exact Lean statement
theorem eq255_equiv_LxRx (h : Equation677 G) (x : G) :
(∃ z, x ◇ (z ◇ x) = z) ↔ (∃ y, y ◇ x = x)Formal artifact
Lean source
theorem eq255_equiv_LxRx (h : Equation677 G) (x : G) : (∃ z, x ◇ (z ◇ x) = z) ↔ (∃ y, y ◇ x = x) := by constructor · rintro ⟨z, hz⟩ exact ⟨x ◇ z, eq677_left_cancel h z (eq677_left_cancel h x ((eq677_leftInv_formula h z x).trans hz.symm))⟩ · rintro ⟨y, hy⟩ refine ⟨y ◇ ((x ◇ y) ◇ x), ?_⟩ have h1 : x ◇ (y ◇ ((x ◇ y) ◇ x)) = y := eq677_leftInv_formula h y x have h2 := eq677_leftInv_formula h (y ◇ ((x ◇ y) ◇ x)) x rwa [h1, hy] at h2- Project
- Equational Theories
- License
- Apache-2.0
- Commit
- 7e276a2d05e8
- Source
- equational_theories/ManuallyProved/Equation677.lean:77-87
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Assoc Implies Sgr Proj Faithful
AssocImpliesSgrProjFaithful
Project documentation
Example usage of AssocFullyRightAssociate -/ theorem Assoc4 {G : Type _} [Magma G] (assoc : Equation4512 G) : ∀ x y z w : G, ((x ◇ y) ◇ z) ◇ w = x ◇ (y ◇ (z ◇ w)) := fun x y z w ↦ AssocFullyRightAssociate assoc (fun | 0 => x | 1 => y | 2 => z | 3 => w : Fin 4 → G) (((Lf 0 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 3) inductive FreeSemigroup (α : Type _) | Singleton : α → FreeS...
Source project: Equational Theories
Person-level attribution pending.
Equation1323 not implies Equation2744
Eq1323.Equation1323_not_implies_Equation2744
Plain-language statement
Source project: Equational Theories
Person-level attribution pending.
Equation374794 not implies Equation2
InfModel.Equation374794_not_implies_Equation2
Plain-language statement
However, Equation374794 doesn't imply Equation2.
Source project: Equational Theories
Person-level attribution pending.