Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Positive representatives of original retained cells

Lax342547.CellRepresentatives · concepts/Lax342547/CellRepresentatives.lean · lax-342547

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    Every retained cell of positive actual mass has a positive-weight orientation representative. A pair of unchanged retained cells therefore supplies representatives for selecting the actual gradient target.

    Concept map
    7 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 positive_cell_member proven

    2 retained_cell_representatives proven

    Lean source view on GitHub

    1import Lax342547.RealCellLaws
    2
    3/-!
    4---
    5title: Positive representatives of original retained cells
    6type: lemma
    7---
    8Every retained cell of positive actual mass has a positive-weight orientation representative. A pair of unchanged retained cells therefore supplies representatives for selecting the actual gradient target.
    9-/
    10
    11namespace Lax342547.CellRepresentatives
    12
    13open Lax342547.RealCellLaws Lax342547.RetainedImages
    14
    15axiom positive_cell_member {Ω : Type} [Fintype Ω]
    16 (ρ : Ω → ℝ) (C : Ω → Prop) (hC : 0 < cellMass ρ C) :
    17 ∃ ω, C ω ∧ 0 < ρ ω
    18
    19axiom retained_cell_representatives {ΩA ΩB : Type} [Fintype ΩA] [Fintype ΩB]
    20 (α : ΩA → ℝ) (β : ΩB → ℝ) (C : ΩA → Prop) (D : ΩB → Prop)
    21 (τ : ℝ) (hτ : 0 < τ) (hC : τ ≤ cellMass α C) (hD : τ ≤ cellMass β D) :
    22 ∃ a b, C a ∧ D b ∧ 0 < α a ∧ 0 < β b
    23
    24end Lax342547.CellRepresentatives
    25
    Show ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…