Project-declaredLean 4.32.1
Inj on of nodup map
FromMathlib.inj_on_of_nodup_map
Plain-language statement
NB. Copied from Mathlib
separation logicprogram logicsemantics
Source project: Iris-Lean
Person-level attribution pending.
Source-pinned research
Research proof index
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 219 research declarations. Search 10,000 more complete Mathlib declarations.
219 results
Clear filtersView proof record
Project-declaredLean 4.32.1
Big Op L hom weak
Iris.Algebra.BigOpL.bigOpL_hom_weak
Plain-language statement
Weak monoid homomorphisms distribute over non-empty big ops.
separation logicprogram logicsemantics
Source project: Iris-Lean
Person-level attribution pending.
Project-declaredLean 4.32.1
Embed internal inj
Iris.BI.embed_internal_inj
Plain-language statement
⎡·⎤ reflects internal equality.
separation logicprogram logicsemantics
Source project: Iris-Lean
Person-level attribution pending.
Project-declaredLean 4.32.1
Mon Pred sbi emp valid exist
Iris.BI.MonPred.monPred_sbi_emp_valid_exist
Plain-language statement
A monotone predicate P is objective if its value does not depend on the index: P i ⊢ P j for all i j. Equivalently P ⊣⊢ <obj> P. -/ @[rocq_alias Objective] class Objective {I : BiIndex} {PROP : Type _} [BI PROP] (P : MonPred I PROP) : Prop where objective_at : ∀ i j : I.car, P.monPred_at i ⊢ P.monPred_at j namespace MonPred variable {I : BiIndex...
separation logicprogram logicsemantics
Source project: Iris-Lean
Person-level attribution pending.
Project-declaredLean 4.32.1
Chain option some
Iris.chain_option_some
Plain-language statement
If a chain of Option is ever some, it is the lift a chain by some.
separation logicprogram logicsemantics
Source project: Iris-Lean
Person-level attribution pending.
Project-declaredLean 4.32.1
Fupd mask frame acc
Iris.fupd_mask_frame_acc
Plain-language statement
A variant of [fupd_mask_frame] that works well for accessors: Tailored to eliminate updates of the form [|={E1,E1∖E2}=> Q] and provides a way to transform the closing view shift instead of letting you prove the same side-conditions twice.
separation logicprogram logicsemantics
Source project: Iris-Lean
Person-level attribution pending.