# Zulip Chat Archive

## Stream: new members

### Topic: Defining a function: size of lower contour.

#### Greg Leo (May 12 2022 at 18:12):

I am trying to define a function that for any `x`

in some finite `A`

returns the size of the set of `y`

in `A`

such that `R x y`

for some relation `R`

. I know how to define some basic functions, and how to define some basic sets, but I can't seem to combine my knowledge to define this function.

#### Patrick Johnson (May 12 2022 at 18:22):

```
import tactic
def f {α : Type} (A : finset α) (x ∈ A) (R : α → α → Prop) [decidable_rel R] : ℕ :=
(A.filter (R x)).card
```

#### Yaël Dillies (May 12 2022 at 18:25):

```
import combinatorics.double_counting
def your_thing {α β : Type*} (r : α → β → Prop) (t : finset β) (a : α) [Π a, decidable (r a b)] :
ℕ :=
(s.bipartite_above r a).card
```

#### Greg Leo (May 12 2022 at 18:31):

I'll need to read about a few things before I understand these. Having two different options should help me figure things out. Thank you!

#### Yaël Dillies (May 12 2022 at 18:33):

The two options are definitionally equal. The advantage of Patrick's is that it's rather transparent in what it does. The advantage of mine is that it directly plugs onto the theory of double-counting.

#### Patrick Johnson (May 12 2022 at 18:49):

They're not definitionally equal, not only because of the order of arguments, but also because they are actually different functions (your definition fixes the second argument of the relation, while mine fixes the first argument).

```
#reduce f {1, 2} 1 dec_trivial (<) -- 1
#reduce your_thing (<) {1, 2} 1 -- 0
```

*"Function that for any x in some finite A returns the size of the set of y in A such that R x y for some relation R"* sounds like

`x`

should be fixed.#### Greg Leo (May 12 2022 at 18:52):

If I was programming it (in some made-up python-like language), I would have something like:

```
f = function(x){
size = 0
for (y in A){
if(R x y){size = size + 1}
}
return(size)
}
```

#### Greg Leo (May 12 2022 at 18:56):

So yeah, `x`

is fixed, and I want to count up the `y`

such that `R x y`

. That is, how many `y`

are there in `A`

that are "worse than" `x`

?

#### Patrick Johnson (May 12 2022 at 18:59):

Then my definition of `f`

is what you need.

#### Yaël Dillies (May 12 2022 at 19:05):

Ah sorry, I meant docs#finset.bipartite_above

Last updated: Dec 20 2023 at 11:08 UTC