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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,387 to 1,392 of 2,569 results.
intermediate_ineq
Mathematical statement
The intermediate operator inequality: ρ_AB ⊗ σ_C⁻¹ ≤ (ρ_A ⊗ σ_BC⁻¹).reindex(assoc⁻¹). This is derived from W_mat_sq_le_one by algebraic manipulation (conjugation and simplification).
Source project: quantumInfo
Person-level attribution pending.
Iris.Algebra.BigOpL.bigOpL_hom_weak
Mathematical statement
Weak monoid homomorphisms distribute over non-empty big ops.
Source project: Iris-Lean
Person-level attribution pending.
Iris.BI.embed_internal_inj
Mathematical statement
⎡·⎤ reflects internal equality.
Source project: Iris-Lean
Person-level attribution pending.
Iris.BI.MonPred.monPred_sbi_emp_valid_exist
Mathematical 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
Mathematical 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.
Iris.fupd_mask_frame_acc
Mathematical 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.
Source project: Iris-Lean
Person-level attribution pending.