Documentation

Mathlib.Tactic.Inclusion.Extension.Core.Core

Core extensions for the inclusion tactic #

This file defines inclusion and hypothesis extensions for the core inclusion family.

source
def Inclusion.instMembershipHyp :
HypothesisExt

HypothesisExt for direct ToSet instance membership hypotheses.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Inclusion.andHyp :
    HypothesisExt

    HypothesisExt for conjunction hypotheses.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For