Source-pinned research
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 19 research declarations. Search 10,000 more complete Mathlib declarations.
19 results
Clear filtersCoPset.coPsetRaw_eq
Plain-language statement
Two CoPsetRaw trees are equal if they have the same membership function and both are well-formed.
Source project: Iris-Lean
Person-level attribution pending.
FromMathlib.inj_on_of_nodup_map
Plain-language statement
NB. Copied from Mathlib
Source project: Iris-Lean
Person-level attribution pending.
Iris.Algebra.BigOpL.bigOpL_hom_weak
Plain-language statement
Weak monoid homomorphisms distribute over non-empty big ops.
Source project: Iris-Lean
Person-level attribution pending.
Iris.BI.embed_internal_inj
Plain-language statement
⎡·⎤ reflects internal equality.
Source project: Iris-Lean
Person-level attribution pending.
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...
Source project: Iris-Lean
Person-level attribution pending.
Iris.chain_option_some
Plain-language statement
If a chain of Option is ever some, it is the lift a chain by some.
Source project: Iris-Lean
Person-level attribution pending.