Project-declaredLean 4.21.0-rc3 · mathlib@5b77ef3c

Support supports coe

ConNF.Support.supports_coe

set theory consistency foundations model data

Plain-language statement

The same as ModelData but without the propositions. -/ class PreModelData (α : TypeIndex) where TSet : Type u AllPerm : Type u [allPermGroup : Group AllPerm] [allAction : MulAction AllPerm TSet] tSetForget : TSet → StrSet α allPermForget : AllPerm → StrPerm α export PreModelData (TSet AllPerm) attribute [instance] PreModelData.allPermGroup PreModelData....

Exact Lean statement

theorem Support.supports_coe {α : Λ} {X : Type _} [PreModelData α] [MulAction (AllPerm α) X]
    (S : Support α) (x : X)
    (h : ∀ ρ : AllPerm α,
      (∀ A : α ↝ ⊥, ∀ a ∈ (S ⇘. A)ᴬ, ρᵁ A • a = a) →
      (∀ A : α ↝ ⊥, ∀ N ∈ (S ⇘. A)ᴺ, ρᵁ A • N = N) → ρ • x = x) :
    S.Supports x

Formal artifact

Lean source

Canonical source

Full Lean sourceLean 4

theorem Support.supports_coe {α : Λ} {X : Type _} [PreModelData α] [MulAction (AllPerm α) X]    (S : Support α) (x : X)    (h : ∀ ρ : AllPerm α,      (∀ A : α ↝ ⊥, ∀ a ∈ (S ⇘. A)ᴬ, ρᵁ A • a = a) →      (∀ A : α ↝ ⊥, ∀ N ∈ (S ⇘. A)ᴺ, ρᵁ A • N = N) → ρ • x = x) :    S.Supports x := by  constructor  · intro ρ h'    apply h    · intro A a ha      exact Enumeration.smul_eq_of_mem_of_smul_eq (smul_atoms_eq_of_smul_eq h') A a ha    · intro A N hN      exact Enumeration.smul_eq_of_mem_of_smul_eq (smul_nearLitters_eq_of_smul_eq h') A N hN  · intro h    cases h

Project: Con(NF)
License: Apache-2.0
Commit: 55b939a3acf9
Source: ConNF/ModelData/ModelData.lean:224-238

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

Project-declaredLean 4.21.0-rc3

Smul near Litter of smul litter

ConNF.BaseAction.smul_nearLitter_of_smul_litter

Project documentation

The main lemma about how approximations interact with actions.

set theoryconsistencyfoundations

Source project: Con(NF)

Person-level attribution pending.

View proof record

Project-declaredLean 4.21.0-rc3

Smul interference

ConNF.BasePerm.smul_interference

Plain-language statement

Base permutations commute with the interference of near-litters.

set theoryconsistencyfoundations

Source project: Con(NF)

Person-level attribution pending.

View proof record

Project-declaredLean 4.21.0-rc3

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.

set theoryconsistencyfoundations

Source project: Con(NF)

Person-level attribution pending.

View proof record