Categorise permutative Extension of one One
Rel.categorise_permutativeExtension_of_oneOne
Plain-language statement
TODO: Strengthen statement in blueprint version.
Exact Lean statement
theorem categorise_permutativeExtension_of_oneOne
{r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) (hr : r.OneOne)
{a₁ a₂ : α} (h : r.permutativeExtension R a₁ a₂) :
r a₁ a₂ ∨ (a₁ ∉ r.dom ∧ a₂ ∉ r.codom ∧ R.categorise a₂ = R.catPerm (R.categorise a₁))Formal artifact
Lean source
theorem categorise_permutativeExtension_of_oneOne {r : Rel α α} (R : OrbitRestriction (r.dom ∪ r.codom) β) (hr : r.OneOne) {a₁ a₂ : α} (h : r.permutativeExtension R a₁ a₂) : r a₁ a₂ ∨ (a₁ ∉ r.dom ∧ a₂ ∉ r.codom ∧ R.categorise a₂ = R.catPerm (R.categorise a₁)) := by by_cases ha₁ : a₁ ∈ r.dom · obtain ⟨b₁, h₁⟩ := ha₁ cases (r.permutativeExtension_permutative R hr).coinjective h (Or.inl h₁) exact Or.inl h₁ by_cases ha₂ : a₂ ∈ r.codom · obtain ⟨b₁, h₁⟩ := ha₂ cases (r.permutativeExtension_permutative R hr).injective h (Or.inl h₁) exact Or.inl h₁ · simp only [ha₁, ha₂, not_false_iff, true_and] exact categorise_permutativeExtension R h- Project
- Con(NF)
- License
- Apache-2.0
- Commit
- 55b939a3acf9
- Source
- ConNF/Background/PermutativeExtension.lean:350-363
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
Smul near Litter of smul litter
ConNF.BaseAction.smul_nearLitter_of_smul_litter
Project documentation
The main lemma about how approximations interact with actions.
Source project: Con(NF)
Person-level attribution pending.
Smul interference
ConNF.BasePerm.smul_interference
Plain-language statement
Base permutations commute with the interference of near-litters.
Source project: Con(NF)
Person-level attribution pending.
Card t Set le
ConNF.card_tSet_le
Plain-language statement
Note that we cannot prove the reverse implication because all of our hypotheses at this stage are about permutations, not objects.
Source project: Con(NF)
Person-level attribution pending.