Documentation

LeanPool.Duality.Common

LeanPool.Duality.Common #

source
theorem Finset.subtype_univ_sum_eq_subtype_univ_sum {α : Type u_1} {β : Type u_2} {p q : α → Prop} (hpq : p = q) [Fintype { a : α // p a }] [Fintype { a : α // q a }] [AddCommMonoid β] {f : { a : α // p a } → β} {g : { a : α // q a } → β} (hfg : ∀ (a : α) (hpa : p a) (hqa : q a), f ⟨a, hpa⟩ = g ⟨a, hqa⟩) :
univ.sum f = univ.sum g
source
theorem Finset.univ_sum_of_zero_when_not {α : Type u_1} {β : Type u_2} [Fintype α] [AddCommMonoid β] {f : α → β} (p : α → Prop) [DecidablePred p] (hpf : ∀ (a : α), ¬p a → f a = 0) :
univ.sum f = ∑ a : { a : α // p a }, f ↑a
source
theorem or_of_neq {P Q : Prop} (hpq : P ≠ Q) :
P ∨ Q
source
theorem not_and_of_neq {P Q : Prop} (hpq : P ≠ Q) :
¬(P ∧ Q)
source
theorem neq_of_iff_neg {P Q : Prop} (hpq : P ↔ ¬Q) :
P ≠ Q
source
theorem neg_iff_neg {P Q : Prop} (hpq : P ↔ Q) :
¬P ↔ ¬Q
source
def «term↓_» :
Lean.ParserDescr

Writing ↓t is slightly more general than writing Function.const _ t.

Equations
Instances For
    source
    def «term_.→» :
    Lean.TrailingParserDescr

    The left-to-right direction of ↔.

    Equations
    Instances For
      source
      def «term_.←» :
      Lean.TrailingParserDescr

      The right-to-left direction of ↔.

      Equations
      Instances For
        source
        theorem le_of_nneg_add {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b c : α} (habc : a + b = c) (ha : 0 ≤ a) :
        b ≤ c
        source
        def tacticChange_To_ :
        Lean.ParserDescr

        change h to t rewrites the hypothesis h to the definitionally equal type t.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def tacticAeply_ :
          Lean.ParserDescr

          aeply t is shorthand for intro <;> apply t <;> aesop, useful for proving universally quantified goals where each instance is dispatched by aesop after applying t.

          Equations
          Instances For